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
180 Open 496 Closed
180 Open 496 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

Nice hierarchical record update syntax. Feature Request Printing-Parsing
#8 opened Sep 5, 2011 by mn200
Fix Induct_on for mutually/nested recursive types Bug Tactics/DPs
#10 opened Sep 5, 2011 by mn200
@mn200
Allow 'raw' option to LaTeX munger commands Feature Request Printing-Parsing
#21 opened Sep 19, 2011 by mn200
@mn200
Allow specification of grammar to LaTeX munger commands Feature Request Printing-Parsing
#22 opened Sep 19, 2011 by mn200
@mn200
Provide in-system documentation for traces Documentation Feature Request
#28 opened Oct 4, 2011 by mn200
New syntax for function-valued fields Feature Request Low Priority Printing-Parsing
#33 opened Oct 4, 2011 by mn200
Use sets rather than lists to store simplifier free variables Feature Request Low Priority Simplifier
#53 opened Feb 2, 2012 by mn200
Define sometimes requires eta-expanded recursive calls Feature Request TFL
#59 opened Apr 8, 2012 by xrchz
Build Miller-Rabin example on top of Concordia's probability theory Feature Request Low Priority Theories
#76 opened Jul 31, 2012 by mn200
Consider using OpenTheory for persistent theories Feature Request
#82 opened Aug 7, 2012 by xrchz
Extend theory graph tool to build graph for more theories
#90 opened Aug 31, 2012 by mn200
minisat on Windows slows build down painfully; invoke it more carefully Feature Request Tactics/DPs
#92 opened Oct 10, 2012 by mn200
Holmake to take -C command-line option Build/Holmake Feature Request Low Priority
#118 opened May 6, 2013 by mn200
quotientLib.define_subset_types undocumented Documentation
#123 opened Jul 1, 2013 by xrchz
analogue of overload_info_for for types Printing-Parsing
#124 opened Jul 1, 2013 by xrchz
Tidy up modularisation in Hol_pp and DB. Feature Request Low Priority Printing-Parsing
#133 opened Nov 3, 2013 by mn200
Methods for user-provided α toto values (for enumfset) Feature Request Theories
#138 opened Dec 16, 2013 by mn200
Simplifier should normalise integer expressions better Feature Request Simplifier
#155 opened Feb 26, 2014 by mn200
Implement multi-session support for Holmake etc Build/Holmake Feature Request Low Priority
#164 opened Apr 24, 2014 by mn200
math mode munger plays badly with inference rules Printing-Parsing
#177 opened Jul 24, 2014 by xrchz
Consider making BAG_IN an overload Feature Request Theories
#181 opened Aug 1, 2014 by mn200
Install monad syntax by default Feature Request Good first issue Printing-Parsing
#211 opened Nov 20, 2014 by mn200
Datatype example fails Bug
#226 opened Jan 20, 2015 by mn200
Possible pretty-printing overload issue Printing-Parsing
#240 opened Mar 3, 2015 by mn200
More datatypes Bounty Feature Request
#266 opened Jul 10, 2015 by xrchz
ProTip! Follow long discussions with comments:>50.