HOL Light with OpenTheory Support (Development Version)

Installing

  1. First, get the development files by cloning the repo:
    mkdir <install-dir>
    cd <install-dir>
    git clone http://src.gilith.com/hol-light
    
  2. Next, initialize this development version of HOL Light:
    cd hol-light
    make
    

Using

All OpenTheory files are located in the opentheory directory. The source files for the theory library are in the opentheory/theories subdirectory, and every theory can be loaded into HOL Light as follows:

ocaml
#use "opentheory/all.ml";;

Updating

Pull the latest version of the development files:

cd <install-dir>/hol-light
git pull