aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Bump yearGravatar David Aspinall2012-02-07
* 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
* New pseudo instances to help tool demonstrators in ocaml/ghci (in progress)Gravatar David Aspinall2012-02-07
* Updated.Gravatar David Aspinall2012-02-07
* Extend list of provers we compile forGravatar 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
* CleanupGravatar David Aspinall2012-02-07
* Set version tag for new release.Gravatar David Aspinall2012-02-06
* Cleaning some code.Gravatar Pierre Courtieu2012-02-01
* Quick fix of a regression introduced by my last commit. Looking for aGravatar Pierre Courtieu2012-02-01
* Fixed command end recognition in presence of operators of the form .+Gravatar Pierre Courtieu2012-02-01
* make sure extra modes availableGravatar David Aspinall2012-01-23
* 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
* TypoGravatar David Aspinall2012-01-19
* Update documentationGravatar David Aspinall2012-01-19
* Added some detail on the indentation limitation in the CHANGE.Gravatar Pierre Courtieu2012-01-18
* Fixed a small bug in indentation (ter repetita). Bullets are indentedGravatar Pierre Courtieu2012-01-18
* Fixed a small bug in indentation (bis repetita).Gravatar Pierre Courtieu2012-01-18
* Fixed a small bug in indentation.Gravatar Pierre Courtieu2012-01-18
* lower cpu utilization of splash screen, see Debian bug #642048Gravatar Hendrik Tews2012-01-14
* Set version tag for new release.Gravatar David Aspinall2012-01-12
* Fix typo, mention HOL LightGravatar David Aspinall2012-01-12
* Adjust license to CC-BY-SA-3Gravatar David Aspinall2012-01-11
* Set version tag for new release.Gravatar David Aspinall2012-01-10
* Tweak message and display model, in particular, make sure that when aGravatar David Aspinall2012-01-10
* Note about make -j for parallel compilationGravatar David Aspinall2012-01-10
* Emphasise importance of TracGravatar David Aspinall2012-01-10
* Mention critical Emacs bug which destroys characters in certainGravatar David Aspinall2012-01-10
* Add documentation for proof-shell-trace-output-regexp (Trac #432) andGravatar David Aspinall2012-01-10
* Support proof-shell-interactive-prompt-regexp, ref Trac #430Gravatar David Aspinall2012-01-10
* Improve configuration for HOL Light. Allow goals display to be prefixed by i...Gravatar David Aspinall2012-01-09
* proof-shell-start-goals-regexp: shy match to avoid introducing match groupGravatar David Aspinall2012-01-09
* proof-shell-end-goals-regexp doc: fix inaccuracy, goals always startGravatar David Aspinall2012-01-09
* Make configuration settings. Tweak error regexp.Gravatar David Aspinall2012-01-06