hol-light - HOL Light interactive theorem prover

       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                                    HOL-LIGHT(1)

       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-lightocaml  toplevel  is
       wrapped  in  readline-editor.  Install just one of these readline editors or configure your preferred one
       via the alternative system.

       hol-light - HOL Light interactive theorem prover

ocaml(1), readline-editor(1), rlwrap(1), ledit(1), rlfe(1)
       HOL Light documentation at http://www.cl.cam.ac.uk/~jrh13/hol-light/

hol-light [options...]