Man page - hol-light(1)

Packages contains this manual

Package:  hol-light
apt-get install hol-light

Manuals in package:
• hol-light(1)
Documentations in package:
• hol-light

Manual

HOL-LIGHT

NAME
SYNOPSIS
DESCRIPTION
SEE ALSO
AUTHOR

---

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).

---