NAME¶
hol-light - HOL Light interactive theorem prover
SYNOPSIS¶
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).