Skip to content

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

License

Notifications You must be signed in to change notification settings

someplaceguy/HOL

 
 

Repository files navigation

Build Status

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

About

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Standard ML 87.2%
  • TeX 11.2%
  • Emacs Lisp 0.7%
  • C++ 0.2%
  • C 0.2%
  • Isabelle 0.1%
  • Other 0.4%