hol-light - Online in the Cloud

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



Latest Linux & Windows online programs