aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol-light
Commit message (Expand)AuthorAge
* Use `cl-lib` instead of `cl` everywhereGravatar Stefan Monnier2018-12-13
* Cleanup patch; Moving defvar to toplevelGravatar Stefan Monnier2018-12-12
* Update copyright messages and improve the header of elisp files.Gravatar Erik Martin-Dorel2018-02-21
* Change (eval-when (compile) ...) to (eval-when-compile ...)Gravatar Clément Pit--Claudel2017-05-05
* Remove compile-time calls to proof-ready-for-assistantGravatar Clément Pit--Claudel2017-03-08
* Fix incorrect assumption that noninteractive == byte-compilingGravatar Clément Pit--Claudel2017-03-08
* Improvements for type tokens, remove preceding colonGravatar David Aspinall2015-01-05
* - support bullets and braces in ProoftreeGravatar Hendrik Tews2013-01-15
* UpdateGravatar David Aspinall2012-11-01
* Remove option aspect of 'finfo' datatype, and rename datatype to 'mldata'.Gravatar mark2012-02-24
* Altered graph .dot export so that nodes are displayed as their tactic.Gravatar mark2012-02-23
* Allocate jobs!Gravatar David Aspinall2012-02-23
* *** empty log message ***Gravatar mark2012-02-23
* Capability for exporting .dot files added.Gravatar mark2012-02-23
* Various small improvements to capabilityGravatar mark2012-02-21
* *** empty log message ***Gravatar David Aspinall2012-02-21
* *** empty log message ***Gravatar David Aspinall2012-02-21
* *** empty log message ***Gravatar David Aspinall2012-02-21
* First version of HOL Light tactic recording.Gravatar mark2012-02-16
* Add example menu entryGravatar David Aspinall2012-02-08
* Duplicate proofGravatar David Aspinall2012-02-08
* Tweak output strings and prompt matchingGravatar David Aspinall2012-02-08
* Abort attempt to use special exception printingGravatar David Aspinall2012-02-08
* Add print_exn for marked up error messages.Gravatar David Aspinall2012-02-08
* Add restart command (does nothing)Gravatar David Aspinall2012-02-08
* Add autotestGravatar David Aspinall2012-02-08
* Fix parenoGravatar David Aspinall2012-02-08
* Add hol-light-prog-name, restart command.Gravatar David Aspinall2012-02-08
* Try to make evars output match what is expected by ProoftreeGravatar David Aspinall2012-02-08
* Add proof-forget-id command and make top_thm discard the goalstack.Gravatar David Aspinall2012-02-08
* Improve handling of undo, implementing pg_kill and pg_undo.Gravatar David Aspinall2012-02-08
* More progress with Prooftree. Basic trees produced. Undoing needs work.Gravatar David Aspinall2012-02-08
* Adjust global state idea, it is supposed to count down as well as up...Gravatar David Aspinall2012-02-08
* Get a little bit further with proof tree.Gravatar David Aspinall2012-02-07
* Load pg_tactics, fix proof-undo-n-times-cmd again.Gravatar David Aspinall2012-02-07
* Borrow syntax keywords from caml-mode if available. Typo in undo-n-times.Gravatar David Aspinall2012-02-07
* Use right HOL systemGravatar David Aspinall2012-02-07
* Attempt to rebind failwith, which fails, with...errorsGravatar David Aspinall2012-02-07
* Fix compileGravatar David Aspinall2012-02-07
* PastoGravatar David Aspinall2012-02-07
* Start support for both plain and custom top levels (work in progress).Gravatar David Aspinall2012-02-07
* Draft symbol handlingGravatar David Aspinall2012-01-23
* Rename goalstate file for pgGravatar David Aspinall2012-01-20
* Rename fileGravatar David Aspinall2012-01-20
* Hint about changing promptGravatar David Aspinall2012-01-20
* Temporary commit to share file, this is work in progress for ProoftreeGravatar David Aspinall2012-01-19
* Add file from MarkGravatar David Aspinall2012-01-19
* Patch needed temporarily to avoid rebuild of ProoftreeGravatar David Aspinall2012-01-19
* Update documentationGravatar David Aspinall2012-01-19
* Improve configuration for HOL Light. Allow goals display to be prefixed by i...Gravatar David Aspinall2012-01-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-19 14:16:02 +0000