aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
Commit message (Expand)AuthorAge
* 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
* tuned;Gravatar Makarius Wenzel2006-12-30
* back again for isar;Gravatar Makarius Wenzel2006-12-07
* isar-keywords-theory-enclose: isar-keywords-theory-switch is back again (in p...Gravatar Makarius Wenzel2006-12-07
* removed obsolete references to 'isa';Gravatar Makarius Wenzel2006-12-07
* proof-shell-pre-interrupt-hook: removed obsolete Poly/ML 3 setup, which break...Gravatar Makarius Wenzel2006-12-07
* X-Symbol config. Moved from isa/Gravatar David Aspinall2006-12-05
* Use Isar-specific isabelle-system fileGravatar David Aspinall2006-12-05
* isar-keywords-theory-enclose: removed isar-keywords-theory-switch, which usua...Gravatar Makarius Wenzel2006-11-04
* isar-strip-terminators, isar-detect-begin: proof-search-forward;Gravatar Makarius Wenzel2006-11-04
* reintroduced pg-subterm-first-special-char, which makes PG strip goal markup;Gravatar Makarius Wenzel2006-10-11
* isar-keywords-indent-enclose: include "begin" keyword;Gravatar Makarius Wenzel2006-10-11
* added regexps for begin/end and theory start;Gravatar Makarius Wenzel2006-10-11
* removed obsolete isar-detect-header;Gravatar Makarius Wenzel2006-10-11
* isar-goals-font-lock-keywords: added abbreviations;Gravatar Makarius Wenzel2006-08-16
* Changed the type of proof-goal-command-p. It takes now a span, whichGravatar Pierre Courtieu2006-04-26