aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
Commit message (Expand)AuthorAge
* Remove use of proof-assGravatar David Aspinall2008-01-24
* Add key binding for ML {* *} and fix longsuper, longsubGravatar David Aspinall2008-01-24
* Updated.Gravatar David Aspinall2008-01-16
* Updated.Gravatar David Aspinall2008-01-16
* Default to using emacs nowGravatar David Aspinall2008-01-15
* Many compatibility updates, bug fixes, rearrangements for compilation.Gravatar David Aspinall2008-01-15
* Move x-symbol-isabelle -> x-symbol-isar to simplify setup.Gravatar David Aspinall2007-12-14
* Deleted fileGravatar David Aspinall2007-12-14
* Typo in pg-special-char-regexpGravatar David Aspinall2007-12-14
* x-symbol-isabelle-prepare-table: specialise to Isar (usefully removes depende...Gravatar David Aspinall2007-12-14
* Remove eval-when, seems unreliableGravatar David Aspinall2007-12-14
* Improve loading; these tests are not functioning yetGravatar David Aspinall2007-12-14
* Make value of pg-special-char-regexp depend on proof-shell-unicode.Gravatar David Aspinall2007-12-14
* Cleanup. Add more insertion commands.Gravatar David Aspinall2007-12-13
* Deleted fileGravatar David Aspinall2007-12-13
* Comment unused functionGravatar David Aspinall2007-12-09
* clarify that -U now defaults to true;Gravatar Makarius Wenzel2007-11-20
* command 'thm' makes no sense outside a proper context;Gravatar Makarius Wenzel2007-11-13
* VersionsGravatar David Aspinall2007-11-12
* proof-shell-issue-pgip-cmd is always isabelle-process-pgip;Gravatar Makarius Wenzel2007-10-24
* removed obsolete isabelle-version-string, isa-version, isa-supports-pgip;Gravatar Makarius Wenzel2007-10-24
* isar-find-and-forget: no special treatment of begin/end, just plain undoGravatar Makarius Wenzel2007-10-18
* isar-undo-fail-regexp: only isar-keywords-control, not isar-keywords-theory-end;Gravatar Makarius Wenzel2007-10-18
* allow more specials: oct 327 .. oct 340;Gravatar Makarius Wenzel2007-09-07
* isar-output-font-lock-keywords-1: hilite markup uses proof-warning-face;Gravatar Makarius Wenzel2007-09-07
* pg-topterm-regexp: use special 376. isar-goalhyplit-test: Delete closing mark...Gravatar David Aspinall2007-08-19
* removed outated comment;Gravatar Makarius Wenzel2007-08-15
* isar-goalhyplit-test: explicit end-marker;Gravatar Makarius Wenzel2007-08-15
* Add support for sending back literal commands reusing PBP markup mechanisms.Gravatar David Aspinall2007-08-14
* isar-improper-regexp: include "prems";Gravatar Makarius Wenzel2007-06-14
* single-char-regexp: tuned symbol regexp;Gravatar Makarius Wenzel2007-06-14
* isar-font-lock-local: tuned symbol regexp;Gravatar Makarius Wenzel2007-06-14
* reverted find theorems default from form to minibufferGravatar weber2007-06-11
* XEmacs 21.4.15 does not seem to know propertizeGravatar weber2007-05-17
* Fix renameGravatar weber2007-05-11
* Fix renameGravatar weber2007-05-11
* works with XEmacs now (ticket #115)Gravatar weber2007-05-11
* Fix renameGravatar David Aspinall2007-05-11
* Rename [proof]find-theorems -> isar-find-theoremsGravatar David Aspinall2007-05-11
* Renamed fileGravatar David Aspinall2007-05-11
* Add experimental find theorems form (not working on all Emacs yet)Gravatar David Aspinall2007-05-10
* New files.Gravatar David Aspinall2007-05-10
* x-symbol-isabelle-font-lock-regexp: demand subsequent non-space character;Gravatar Makarius Wenzel2007-05-08
* undo: removed confusing comment;Gravatar Makarius Wenzel2007-05-08
* tuned cannot-undo;Gravatar Makarius Wenzel2007-05-08
* added isar-cmd-sledgehammer;Gravatar Makarius Wenzel2007-05-08
* tuned pg-special-char-regexp;Gravatar Makarius Wenzel2007-05-08
* Patch for XEmacs 21.5 beta match-replace bugGravatar David Aspinall2007-03-03
* Fix commentGravatar David Aspinall2007-02-28
* Comment about undo; useGravatar David Aspinall2007-01-10