Issues

• Expose reliable Theory.dat parent identities and validation for build tools

  HOL-Theorem-Prover/HOL#2068 · Filter by author xrchz opened on Oct 3, 2026

• Implement meson_split_limit for meson

  Tactics/DPs
  HOL-Theorem-Prover/HOL#2062 · Filter by author ordinarymath opened on Sep 15, 2026
  

• Explore alternative design for records

  HOL-Theorem-Prover/HOL#2061 · Filter by author IlmariReissumies opened on Sep 15, 2026

• Expose structural NOT_MEM_CONV and ALL_DISTINCT_CONV from a general list library

  HOL-Theorem-Prover/HOL#2057 · Filter by author xrchz opened on Sep 8, 2026

• Share tactic-step infrastructure between TacticParse/goalFrag and holbuild Proof IR

  HOL-Theorem-Prover/HOL#2056 · Filter by author xrchz opened on Sep 8, 2026
  6

• Improve speed of PMATCH_INTRO_CONV and PMATCH_ELIM_CONV in patternMatchesLib

  HOL-Theorem-Prover/HOL#2052 · Filter by author ordinarymath opened on Sep 5, 2026
  2

• Expose a staged/custom-prover API for explicit termination proofs

  HOL-Theorem-Prover/HOL#2043 · Filter by author xrchz opened on Aug 28, 2026
  2

• Axiom nonce reuse make axiom tracking difficult

  Kernel
  HOL-Theorem-Prover/HOL#2028 · Filter by author xrchz opened on Jul 23, 2026
  1

• mk_EqualityType_ind missing *_def theorem for imported mutual datatype

  HOL-Theorem-Prover/HOL#2015 · Filter by author xxnapaxx opened on Jun 27, 2026
  3

• Improve termination proof automation

  HOL-Theorem-Prover/HOL#2008 · Filter by author konrad-slind opened on Jun 3, 2026

• Proposal: disallow multiple subgoals with THEN

  HOL-Theorem-Prover/HOL#1957 · Filter by author xrchz opened on May 8, 2026
  8

• Bad interaction between not guessing overloads and first_x_assum

  HOL-Theorem-Prover/HOL#1956 · Filter by author dnezam opened on May 8, 2026
  1

• DB.match should try all of the patterns that overloading would generate

  HOL-Theorem-Prover/HOL#1952 · Filter by author dnezam opened on May 7, 2026
  2

• Add FLOOKUP_SIMP as simp

  HOL-Theorem-Prover/HOL#1951 · Filter by author dnezam opened on May 5, 2026

• Add mechanism to deprecate constants/types in a backwards compatible manner

  HOL-Theorem-Prover/HOL#1924 · Filter by author dnezam opened on Apr 25, 2026
  1

• Replace per-directory Holmakefiles with toplevel holproject.toml

  HOL-Theorem-Prover/HOL#1916 · Filter by author charles-cooper opened on Apr 21, 2026
  2

• Syntax highlighting for HOL

  HOL-Theorem-Prover/HOL#1849 · Filter by author digama0 opened on Mar 4, 2026
  3

• Add goal view to LSP server

  HOL-Theorem-Prover/HOL#1848 · Filter by author digama0 opened on Mar 4, 2026
  6

• Make LSP server use the new parser

  HOL-Theorem-Prover/HOL#1846 · Filter by author digama0 opened on Mar 4, 2026
  1

• Platform exploitation is hard to prevent/detect (soundness issue)

  HOL-Theorem-Prover/HOL#1841 · Filter by author xrchz opened on Mar 1, 2026
  4

• Feature: Nonlinear Arithmetic (Sum-of-Squares)

  HOL-Theorem-Prover/HOL#1831 · Filter by author charles-cooper opened on Feb 22, 2026
  8

• feature request: (more) incremental builds

  HOL-Theorem-Prover/HOL#1827 · Filter by author charles-cooper opened on Feb 18, 2026
  2

• Add wrapper constant to identify record access/update

  HOL-Theorem-Prover/HOL#1818 · Filter by author talsewell opened on Feb 10, 2026

• Stronger LET defncong rule doesn't work.

  TFL
  HOL-Theorem-Prover/HOL#1813 · Filter by author ordinarymath opened on Feb 4, 2026
  8

• Implement non-emptiness witness storage and composition

  HOL-Theorem-Prover/HOL#1812 · Filter by author mn200 opened on Feb 4, 2026