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.
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
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
General modern "quotation" syntax support
Feature Request
Printing-Parsing
#1229
opened May 1, 2024 by
mn200
Add spec form to cover both
INST
and SPEC
of theorems
Feature Request
#1221
opened Apr 11, 2024 by
mn200
Ignore assumption directive for simplifier
Feature Request
Simplifier
#1220
opened Apr 11, 2024 by
mn200
Tools should report config files' location
Feature Request
Good first issue
#1141
opened Aug 25, 2023 by
mn200
Use kernel compute feature in HOL4 simplifier, decision procedures, and EVAL
Feature Request
#1118
opened Jun 28, 2023 by
myreen
emacs mode: package the lisp code for it to be released in a package archive
#1103
opened Apr 19, 2023 by
chenzhawyang
emacs mode should choose HOL executable based on lastmaker file (if any)
Editor modes
#1101
opened Apr 6, 2023 by
mn200
Store location information about where theorems were proved in Theory.sig files
Editor modes
Feature Request
#1094
opened Feb 14, 2023 by
mn200
qmatch_abbrev_tac should rename var/var bindings rather than abbreviate them
Feature Request
Tactics/DPs
#1085
opened Jan 5, 2023 by
mn200
Update Definition syntaxes to allow declaration of types of new constants
Feature Request
#1065
opened Oct 26, 2022 by
mn200
Make ability to use "transient" (deleted on export) definitions easier for users
#1062
opened Oct 25, 2022 by
mn200
Creating a conversion of indefinite integrals (antiderivatives) of real functions
#1052
opened Jul 7, 2022 by
binghe
Previous Next
ProTip!
Find all open issues with in progress development work with linked:pr.