hol-light1
Hol light interactive theorem prover
Usage
hol-light [options ...]
Overview
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.
Releases
Unchanged in 6 releases since Debian 7 (Wheezy).