.\"                                      Hey, EMACS: -*- nroff -*-
.\" First parameter, NAME, should be all caps
.\" Second parameter, SECTION, should be 1-8, maybe w/ subsection
.\" other parameters are allowed: see man(7), man(1)
.TH HOL-LIGHT 1 "March  16, 2012"
.\" Please adjust this date whenever revising the manpage.
.\"
.\" Some roff macros, for reference:
.\" .nh        disable hyphenation
.\" .hy        enable hyphenation
.\" .ad l      left justify
.\" .ad b      justify to both left and right margins
.\" .nf        disable filling
.\" .fi        enable filling
.\" .br        insert line break
.\" .sp <n>    insert n+1 empty lines
.\" for manpage-specific macros, see man(7)
.SH NAME
hol-light \- HOL Light interactive theorem prover
.SH SYNOPSIS
.B hol-light
.RI "[options...]"
.SH DESCRIPTION
The command
.B hol-light
is a simple wrapper for calling 
.B ocaml
and loading the HOL Light basic definitions (by loading
.I /usr/share/hol-light/hol.ml
instead of 
.B .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
.B ocaml\fR.
.\"==========================================================================
.P
If you have a 
.B readline-editor
such as
.B rlwrap\fR, \fBledit\fR or \fBrlfe
installed, the 
.B hol-light ocaml
toplevel is wrapped in
.B readline-editor\fR.
Install just one of these readline editors or configure your
preferred one via the alternative system.
.SH SEE ALSO
.BR ocaml "(1), " readline-editor "(1), " rlwrap "(1), " ledit "(1), " rlfe (1)
.br
HOL Light documentation at 
.I http://www.cl.cam.ac.uk/~jrh13/hol-light/
.SH AUTHOR
The 
.B 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).