This is the command hol-light that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator
PROGRAM:
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.
Use hol-light online using onworks.net services
