Skip to content

Issues: HOL-Theorem-Prover/HOL

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clear current search query, filters, and sorts
10 Open 33 Closed
10 Open 33 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Deprecate adjoin_to_theory
#1383 opened Jan 7, 2025 by xrchz
@mn200 @xrchz
8
Pretty-printing of quantified formula is gross Bug Printing-Parsing
#1361 opened Dec 4, 2024 by mn200
@mn200
Holmake to rebuild based on theory hashes rather than timestamps Build/Holmake Feature Request
#381 opened Nov 30, 2016 by xrchz
@mn200
8
More precise control of Holmake --fast Build/Holmake Feature Request
#371 opened Nov 15, 2016 by SOwens
@mn200
1
Binder-like syntax for {PROD,SUM}_IMAGE Feature Request Printing-Parsing
#51 opened Jan 11, 2012 by mn200
@mn200
1
Allow specification of grammar to LaTeX munger commands Feature Request Printing-Parsing
#22 opened Sep 19, 2011 by mn200
@mn200
Allow 'raw' option to LaTeX munger commands Feature Request Printing-Parsing
#21 opened Sep 19, 2011 by mn200
@mn200
Fix Induct_on for mutually/nested recursive types Bug Tactics/DPs
#10 opened Sep 5, 2011 by mn200
@mn200
Allow pattern-overloading to work with paired abstractions Feature Request Printing-Parsing
#9 opened Sep 5, 2011 by mn200
@mn200
3
Handle paired-abstractions better Feature Request Simplifier
#7 opened Sep 5, 2011 by mn200
@mn200
4
ProTip! Find all open issues with in progress development work with linked:pr.