Skip to content

@HOL-Theorem-Prover HOL Theorem Proving System

Change the repository type filter

All

    Repositories list

    6 repositories

    • HOL

      Public
      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.
      lambda-calculustheorem-provinghigher-order-logic
      Standard ML
      •
      Other
      •163•713•240•15•Updated Jan 13, 2026Jan 13, 2026

    • hol-webpages

      Public
      Webpages for the HOL4 website (currently at hol-theorem-prover.org)
      HTML
      •10•3•2•0•Updated Oct 19, 2025Oct 19, 2025

    • armv8.6-asl-snapshot

      Public
      Standard ML
      •2•2•0•0•Updated Oct 2, 2025Oct 2, 2025

    • hol4-vscode

      Public
      HOL4 mode for VSCode
      TypeScript
      •5•5•1•2•Updated Jul 29, 2025Jul 29, 2025

    • hol-guidebook

      Public
      HOL Guidebook
      CSS
      •7•11•1•0•Updated Oct 11, 2024Oct 11, 2024

    • SublimeHOL

      Public
      SublimeHOL - A HOL Development Environment built on top of SublimeREPL
      Python
      •
      Other
      •311•2•0•0•Updated Sep 7, 2019Sep 7, 2019