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
21 Open 131 Closed
21 Open 131 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

Auto-indent incorrectly indents comments and overloads if they follow theorems defined using SPEC ... Bug Editor modes
#1480 opened May 3, 2025 by Eric-C-Hall
defncong adds cong twice Bug
#1413 opened Feb 28, 2025 by xrchz
4
Pretty-printing of quantified formula is gross Bug Printing-Parsing
#1361 opened Dec 4, 2024 by mn200
@mn200
Local theorems don't show up in search results Bug
#1350 opened Nov 20, 2024 by myreen
1
Case expression prints badly Bug Printing-Parsing
#1086 opened Jan 10, 2023 by mn200
1
Record package's "forall" theorem is wrong for polymorphic records Bug
#906 opened Apr 7, 2021 by mn200
Pattern-matching compilation fails Bug TFL
#830 opened Jun 16, 2020 by mn200
1
Congruence rule in TFL depends on bound variable Bug TFL
#681 opened Mar 24, 2019 by mn200
3
Arithmetic normalisation involving two subtractions fails if either can't be moved Bug Simplifier Tactics/DPs
#674 opened Mar 4, 2019 by mn200
Arithmetic normalisation of subtraction + SUC doesn't Bug Simplifier Tactics/DPs
#672 opened Mar 4, 2019 by mn200
1
Restricted quantifier pretty-printing failure Bug Printing-Parsing
#532 opened May 1, 2018 by mn200
Moscow ML build fails TeX selftest Bug
#468 opened Oct 4, 2017 by mn200
Emacs hangs when using mark tactic twice or inside a term Bug
#422 opened May 19, 2017 by Luceat
2
Link to Definition.new_type_definition is missing from HTML index of symbolic identifiers Bug Documentation Low Priority
#238 opened Feb 24, 2015 by ptroja
1
Datatype example fails Bug
#226 opened Jan 20, 2015 by mn200
Quantification over Define's result Bug Low Priority TFL
#186 opened Aug 11, 2014 by mn200
3
Termination prover not strong enough Bug TFL
#101 opened Nov 3, 2012 by acjf3
9
TypeBasePure.gen_datatype_info undocumented Bug Documentation TFL
#65 opened May 26, 2012 by xrchz
3
Defining recursive Monadic functions Bug TFL
#63 opened May 22, 2012 by acjf3
2
EmitML prints types with reserved words Bug Low Priority
#56 opened Apr 2, 2012 by xrchz
4
Fix Induct_on for mutually/nested recursive types Bug Tactics/DPs
#10 opened Sep 5, 2011 by mn200
@mn200
ProTip! no:milestone will show everything without a milestone.