aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/isar.el
Commit message (Expand)AuthorAge
...
* Remove proof-no-commandGravatar David Aspinall2009-09-04
* Doc fixesGravatar David Aspinall2009-08-31
* Prevent reporting column number back to Isabelle processGravatar David Aspinall2009-08-31
* Quick fix to isar-remove-file, see trac #274Gravatar David Aspinall2009-08-31
* isar-positions-of: skip whitespace before command startGravatar David Aspinall2009-08-29
* isar-nonwrap-regexp: ML should work (note that there are *many* ML commands);Gravatar Makarius Wenzel2009-08-28
* Fix compile warningsGravatar David Aspinall2009-08-28
* CommentsGravatar David Aspinall2009-08-28
* Add menu entry for setting proof assistant commandGravatar David Aspinall2009-08-25
* Enhance command markup to pass position information. Extend defaults for res...Gravatar David Aspinall2009-08-19
* Hints about setting position in commandGravatar David Aspinall2009-08-18
* First attempt at command wrapping (see http://proofgeneral.inf.ed.ac.uk/trac/...Gravatar David Aspinall2009-08-18
* TidyGravatar David Aspinall2009-08-17
* Set proof-query-identifier-command in right place.Gravatar David Aspinall2009-08-14
* Rename proof-shell-identifier-under-mouse-cmd -> proof-query-identifier-commandGravatar David Aspinall2009-08-07
* Add configuration setting for Find Theorems formGravatar David Aspinall2009-08-06
* Set strip-output-function for pasting. Adjust font-lock handling toGravatar David Aspinall2009-05-26
* Add proof-electric-terminator-noterminator behaviour for IsarGravatar David Aspinall2009-05-26
* Rename isatool -> isabelleGravatar David Aspinall2009-05-26
* eliminated obsolete non-ASCII specials;Gravatar Makarius Wenzel2009-03-31
* Merge changes from Version4Branch.Gravatar David Aspinall2008-07-24
* Use proof-guess-command-line to adjust command line when starting Isabelle.Gravatar David Aspinall2008-07-10
* Start to rationalise setting for proof-prog-name.Gravatar David Aspinall2008-07-10
* Remove isar-activate-scripting, which was identical to defaultGravatar David Aspinall2008-02-17
* Set proof-shell-eager-annotation-start-length=2. This should have beenGravatar David Aspinall2008-02-17
* Add mode documentationGravatar David Aspinall2008-02-04
* Set proof-shell-trace-output-regexp early enough to have effect. Fixes trac ...Gravatar David Aspinall2008-01-29
* Add key binding for ML {* *} and fix longsuper, longsubGravatar David Aspinall2008-01-24
* 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
* Typo in pg-special-char-regexpGravatar David Aspinall2007-12-14
* Make value of pg-special-char-regexp depend on proof-shell-unicode.Gravatar David Aspinall2007-12-14
* proof-shell-issue-pgip-cmd is always isabelle-process-pgip;Gravatar Makarius Wenzel2007-10-24
* isar-find-and-forget: no special treatment of begin/end, just plain undoGravatar Makarius Wenzel2007-10-18
* allow more specials: oct 327 .. oct 340;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
* reverted find theorems default from form to minibufferGravatar weber2007-06-11
* Rename [proof]find-theorems -> isar-find-theoremsGravatar David Aspinall2007-05-11
* Add experimental find theorems form (not working on all Emacs yet)Gravatar David Aspinall2007-05-10
* 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
* Use Isar-specific isabelle-system fileGravatar David Aspinall2006-12-05
* 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
* removed obsolete isar-detect-header;Gravatar Makarius Wenzel2006-10-11