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

ordinarymath/HOL

This branch is 294 commits behind HOL-Theorem-Prover/HOL:develop.

Folders and files

NameName
Last commit message
Last commit date

Latest commit

3897f56 · Feb 24, 2025
Jan 29, 2025
Jan 30, 2025
Feb 15, 2018
Nov 22, 2024
Nov 14, 2024
Feb 20, 2025
Feb 24, 2025
Feb 1, 2009
Feb 24, 2025
Dec 11, 2024
Jan 22, 2025
Mar 10, 2022
Feb 20, 2025
Feb 26, 2019
Oct 21, 2024
Mar 6, 2017
Jan 4, 2023
Jun 29, 2023

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

Packages

No packages published

Languages

  • Standard ML 87.8%
  • TeX 9.8%
  • Emacs Lisp 0.7%
  • JetBrains MPS 0.6%
  • C 0.2%
  • C++ 0.2%
  • Other 0.7%