HOL-Theorem-Prover/HOL

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.

Source code at GitHub https://hol-theorem-prover.org

{
  "createdAt": "2009-10-29T02:47:31Z",
  "defaultBranch": "develop",
  "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.",
  "fullName": "HOL-Theorem-Prover/HOL",
  "homepage": "https://hol-theorem-prover.org",
  "language": "Standard ML",
  "name": "HOL",
  "pushedAt": "2025-11-25T06:46:37Z",
  "stargazersCount": 698,
  "topics": [
    "higher-order-logic",
    "lambda-calculus",
    "theorem-proving"
  ],
  "updatedAt": "2025-11-25T06:46:42Z",
  "url": "https://github.com/HOL-Theorem-Prover/HOL"
}

This is the distribution directory for 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