aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol-light/hol-light.el
Commit message (Collapse)AuthorAge
* - support bullets and braces in ProoftreeGravatar Hendrik Tews2013-01-15
| | | | - prooftree protocol change to version 3
* Add example menu entryGravatar 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
|
* Fix parenoGravatar David Aspinall2012-02-08
|
* Add hol-light-prog-name, restart command.Gravatar 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
|
* 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
|
* 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
|
* Rename goalstate file for pgGravatar David Aspinall2012-01-20
|
* Temporary commit to share file, this is work in progress for ProoftreeGravatar David Aspinall2012-01-19
|
* Improve configuration for HOL Light. Allow goals display to be prefixed by ↵Gravatar David Aspinall2012-01-09
| | | | ignored junk (val it : goalstack =).
* Make configuration settings. Tweak error regexp.Gravatar David Aspinall2012-01-06
|
* Some fixes to get a working instance for HOL Light. Work in progress.Gravatar David Aspinall2012-01-05
|
* Experimental hol-light version, not usable yetGravatar David Aspinall2010-09-29