Provided by: hol-light_20190729-2build1_amd64 bug


       hol-light - HOL Light interactive theorem prover


       hol-light [options...]


       The  command  hol-light  is  a  simple wrapper for calling ocaml and loading the HOL Light
       basic  definitions  (by  loading  /usr/share/hol-light/  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.


       ocaml(1), readline-editor(1), rlwrap(1), ledit(1), rlfe(1)
       HOL Light documentation at


       The hol-light script and this manual page were written by Hendrik Tews <>,
       specifically for the Debian project (and may be used by others).

                                         March  16, 2012                             HOL-LIGHT(1)