aboutsummaryrefslogtreecommitdiff
path: root/isar/isar.el
AgeCommit message (Expand)Author
2007-10-24proof-shell-issue-pgip-cmd is always isabelle-process-pgip;Makarius Wenzel
2007-10-18isar-find-and-forget: no special treatment of begin/end, just plain undoMakarius Wenzel
2007-09-07allow more specials: oct 327 .. oct 340;Makarius Wenzel
2007-08-19pg-topterm-regexp: use special 376. isar-goalhyplit-test: Delete closing mark...David Aspinall
2007-08-15removed outated comment;Makarius Wenzel
2007-08-15isar-goalhyplit-test: explicit end-marker;Makarius Wenzel
2007-08-14Add support for sending back literal commands reusing PBP markup mechanisms.David Aspinall
2007-06-11reverted find theorems default from form to minibufferweber
2007-05-11Rename [proof]find-theorems -> isar-find-theoremsDavid Aspinall
2007-05-10Add experimental find theorems form (not working on all Emacs yet)David Aspinall
2007-05-08tuned cannot-undo;Makarius Wenzel
2007-05-08added isar-cmd-sledgehammer;Makarius Wenzel
2007-05-08tuned pg-special-char-regexp;Makarius Wenzel
2007-03-03Patch for XEmacs 21.5 beta match-replace bugDavid Aspinall
2006-12-05Use Isar-specific isabelle-system fileDavid Aspinall
2006-11-04isar-strip-terminators, isar-detect-begin: proof-search-forward;Makarius Wenzel
2006-10-11reintroduced pg-subterm-first-special-char, which makes PG strip goal markup;Makarius Wenzel
2006-10-11removed obsolete isar-detect-header;Makarius Wenzel
2006-04-26Changed the type of proof-goal-command-p. It takes now a span, whichPierre Courtieu
2006-02-12isar-preprocessing: replace \n by \<^newline>;Makarius Wenzel
2005-09-28old specials are recogized again;Makarius Wenzel
2005-09-21Tweak.David Aspinall
2005-09-21Add command menuDavid Aspinall
2005-09-17proof-shell-wakeup-char ?\^AMakarius Wenzel
2005-09-14removed 8bit special chars for isar;Makarius Wenzel
2005-09-01renamed thms_containing to find_theorems;Makarius Wenzel
2005-09-01special regexps: include PGASCII version;Makarius Wenzel
2005-08-26proof-defshortcut isar-local: \<^loc>;Makarius Wenzel
2005-08-14Fix isar-shell-adjust-line-width for mutliple frame mode.David Aspinall
2005-08-09next-error-regexp seems to have broken; fix it against current Isabelle CVS.David Aspinall
2005-08-08proof-defshortcut isar-bold;Makarius Wenzel
2005-05-22removed find_rwrites, print_intros;Makarius Wenzel
2005-02-15Changes from Clemens Ballarin for large X-Symbol fontsDavid Aspinall
2004-10-07Remove print draft from menuDavid Aspinall
2004-07-23Fix display_drafts -> print_draftsDavid Aspinall
2004-06-17Fix index number back for isar-undo-remove-regexp, change isar-remove instead.David Aspinall
2004-06-16Fix error regexps for matching additional comma printed in position [NB: for ...David Aspinall
2004-06-16Last change: added also isar-display-draft isar-print-draft forDavid Aspinall
2004-06-16Fix for name matching changes grouping in isar-undo-remove-regexp.David Aspinall
2004-06-13Add functions for displaying/printing draft.David Aspinall
2004-05-09Set comment-quote-nested (for Emacs/XEmacs 21.5)David Aspinall
2004-05-06Patch from Brother MakariusDavid Aspinall
2004-04-17Add shortcuts for new X-Symbol sequences.David Aspinall
2004-04-17Add proof-cannot-reopen-processed-files to fix behaviour of multiple files fo...David Aspinall
2004-04-15Set imenu-syntax-alist. Seems to solve prefix/underscore issue in SpeedbarDavid Aspinall
2004-04-14Add imenu support.David Aspinall
2004-04-14Fix to proof-goal-with-hole-result to agree with isar-syntax.elDavid Aspinall
2004-04-14fixed regexp problem with function menuGerwin Klein
2004-04-13Set proof-goal-with-hole-result to account for use of shy grouping in goal-wi...David Aspinall
2004-02-08Update email and web addressesDavid Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 13:55:09 +0000