table of contents
HOL-LIGHT(1) | General Commands Manual | HOL-LIGHT(1) |
NAME¶
hol-light - HOL Light interactive theorem proverSYNOPSIS¶
hol-light [options...]DESCRIPTION¶
The command hol-light is a simple wrapper for calling ocaml and loading the HOL Light basic definitions (by loading /usr/share/hol-light/hol.ml instead of .ocamlinit as initialization file). Loading these definitions takes about 2 minutes on modern hardware, please be patient. All options and other arguments are passed as options to ocaml.If you have a readline-editor such as rlwrap, ledit or rlfe installed, the hol-light ocaml toplevel is wrapped in readline-editor. Install just one of these readline editors or configure your preferred one via the alternative system.
SEE ALSO¶
ocaml(1), readline-editor(1), rlwrap(1), ledit(1), rlfe(1)HOL Light documentation at http://www.cl.cam.ac.uk/~jrh13/hol-light/
AUTHOR¶
The hol-light script and this manual page were written by Hendrik Tews <hendrik@askra.de>, specifically for the Debian project (and may be used by others).March 16, 2012 |