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.

Notifications You must be signed in to change notification settings

kth-step/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

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Standard ML 80.5%
  • TeX 13.9%
  • OCaml 4.0%
  • Emacs Lisp 0.4%
  • C++ 0.3%
  • C 0.3%
  • Other 0.6%