Need help with HOL?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

HOL-Theorem-Prover
420 Stars 80 Forks Other 17.9K Commits 144 Opened issues

Description

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.

Services available

!
?

Need anything else?

Contributors list

# 197,793
theorem...
TeX
OCaml
lambda-...
8230 commits
# 349,640
theorem...
TeX
OCaml
lambda-...
1550 commits
# 356,220
theorem...
TeX
OCaml
lambda-...
1289 commits
# 204,333
Shell
theorem...
OCaml
sed
1149 commits
# 454,720
theorem...
TeX
OCaml
lambda-...
497 commits
# 467,111
theorem...
TeX
OCaml
lambda-...
457 commits
# 273,602
theorem...
OCaml
Shell
sed
420 commits
# 515,046
theorem...
OCaml
C++
lambda-...
225 commits
# 245,871
Common ...
theorem...
lambda-...
Shell
204 commits
# 562,286
theorem...
OCaml
C++
lambda-...
165 commits
# 583,308
theorem...
OCaml
C++
lambda-...
130 commits
# 487,820
theorem...
OCaml
lambda-...
Shell
100 commits
# 604,008
theorem...
OCaml
C++
lambda-...
99 commits
# 624,996
theorem...
OCaml
C++
lambda-...
84 commits
# 681,073
theorem...
OCaml
C++
lambda-...
44 commits
# 671,948
theorem...
OCaml
C++
lambda-...
42 commits
# 173,938
opam
Haskell
lexer-g...
pretty-...
41 commits
# 690,158
theorem...
OCaml
C++
lambda-...
39 commits
# 586,631
Shell
sed
OCaml
formal-...
36 commits
# 274,474
OCaml
Shell
Common ...
theorem...
34 commits

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

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.