Hi, | How can i running the NAME.ml file in HOl-Light?
You can just use the OCaml #use construct, e.g. #use "NAME.ml";; though you may prefer a HOL Light specific alternative "loadt". This also loads from some system search paths if the file is not in the current directory: loadt "NAME.ml";; | How can I generate a proof article file from running the NAME.ml file in | HOL-Light? There are no special ways to produce any kind of document from the ML files. The theorem statements themselves will be printed as the file is loaded, and you can fairly easily edit this into LaTeX or whatever if you want to include it in a paper. John. ------------------------------------------------------------------------------ The Planet: dedicated and managed hosting, cloud storage, colocation Stay online with enterprise data centers and the best network in the business Choose flexible plans and management services without long-term contracts Personal 24x7 support from experience hosting pros just a phone call away. http://p.sf.net/sfu/theplanet-com _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
