Canonical sources for HOL4 theorem-proving system. Branch master is where "mainline development" occurs.
Standard ML PostScript TeX OCaml C++ C Other
Latest commit f6f2f85 Feb 22, 2017 @mn200 mn200 Tweak some Interaction guide text
Including:
- prefer qexists_tac to Q.EXISTS_TAC, and rpt strip_tac to REPEAT
  STRIP_TAC
- mention possibility of Induct_on `term`

Still to do:
- recommend simp, fs, and rfs rather than the current discussion of
  using std_ss. bool_ss etc
- maybe mention suffices_by

README

This is the distribution directory for the Kananaskis release of HOL4.
See http://hol-theorem-prover.org for online resources.

The following is a brief listing of what's available in the distribution.

     INSTALL        * Installation instructions
     COPYRIGHT      * Copyright notice
     std.prelude    * File loaded at the beginning of each HOL session

     bin/           * Executables
     doc/           * Some documentation, including release notes
     examples/      * Some examples
     help/          * Help support
     src/           * The system sources
     tools/         * Support for building the system
     sigobj/        * Collection of all signatures and compiled code