aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
Commit message (Expand)AuthorAge
* Failed attempted hack to support ML files in isar mode (see comments in isar-...Gravatar David Aspinall2000-06-07
* Allowed ; to terminate a command by including it in regexp for cmdstartGravatar David Aspinall2000-06-06
* isar-save-with-hole-regexp: proof-no-regexp;Gravatar Makarius Wenzel2000-06-05
* proof-indent-commands-regexp: use proof-no-regexp;Gravatar Makarius Wenzel2000-06-05
* Removed defunct commentsGravatar David Aspinall2000-06-05
* Temporary bug fix to solve nil span error messageGravatar David Aspinall2000-06-05
* replaced isar-verbatim by isabelle-verbatim;Gravatar Makarius Wenzel2000-06-04
* updated;Gravatar Makarius Wenzel2000-06-04
* replaced isar-verbatim by isabelle-verbatim;Gravatar Makarius Wenzel2000-06-04
* { } are back;Gravatar Makarius Wenzel2000-06-03
* Removed now spurious semicolons, 8-).Gravatar David Aspinall2000-06-01
* Temporarily removed keywords { and } for new parsing mechanismGravatar David Aspinall2000-06-01
* Remove setting of proof-segment-up-toGravatar David Aspinall2000-06-01
* improved isar-goals-font-lock-keywords;Gravatar Makarius Wenzel2000-05-30
* isar-preprocessing inserts final terminator if none there.Gravatar David Aspinall2000-05-30
* Tweak font lock exprs enough for Example.thyGravatar David Aspinall2000-05-29
* Font lock exprs for goals buffer like those in IsabelleGravatar David Aspinall2000-05-29
* Set settings format function before calculating initial command. Add hilit f...Gravatar David Aspinall2000-05-29
* Use generic default setting mechanism now. Add isar-markup-ml here.Gravatar David Aspinall2000-05-29
* Add -*- isar -*- tag to force mode, and comment to explain.Gravatar David Aspinall2000-05-29
* isar-any-command-regexp;Gravatar Makarius Wenzel2000-05-26
* isar-keywords-major;Gravatar Makarius Wenzel2000-05-26
* Removed spurious code in isar-mode function.Gravatar David Aspinall2000-05-25
* Patch for synchronization problem in Coq, perhaps others.Gravatar David Aspinall2000-05-25
* added "done";Gravatar Makarius Wenzel2000-05-24
* replaced proof-ids-to-regexp by isar-ids-to-regexp, which admitsGravatar Makarius Wenzel2000-05-22
* replaced {{ }} by { };Gravatar Makarius Wenzel2000-05-22
* isar-verbatim-regexp: include \n;Gravatar Makarius Wenzel2000-05-19
* re-use isa/interface-setup.el rather than separate isar version;Gravatar Makarius Wenzel2000-05-17
* Move setting of proof-shell-pre-interrupt-hook to isabelle-system.elGravatar David Aspinall2000-05-16
* Modification of proof-shell-init-cmd. Markus, please help...Gravatar David Aspinall2000-05-12
* Load isabelle-system file shared with Isabelle Proof General.Gravatar David Aspinall2000-05-11
* Default to isa-mode or isar-mode according to first one invoked.Gravatar David Aspinall2000-05-05
* isar-indent regexps moved to isar-syntax.el;Gravatar Makarius Wenzel2000-04-25
* removed unused isar-ids;Gravatar Makarius Wenzel2000-04-25
* removed "simpset" minor keyword;Gravatar Makarius Wenzel2000-04-25
* added 'hide';Gravatar Makarius Wenzel2000-04-17
* fixed proof-mode-for-goals;Gravatar Makarius Wenzel2000-04-12
* pbp-mode -> goals-modeGravatar David Aspinall2000-04-07
* tuned \<bottom>;Gravatar Makarius Wenzel2000-04-06
* tuned todo stuff;Gravatar Makarius Wenzel2000-04-05
* improved print_mode switch;Gravatar Makarius Wenzel2000-04-05
* 'welcome' made diagnostic;Gravatar Makarius Wenzel2000-04-05
* eliminated 'as' keyword;Gravatar Makarius Wenzel2000-04-05
* added 'print_claset', 'print_simpset';Gravatar Makarius Wenzel2000-04-04
* added 'ProofGeneral.undo';Gravatar Makarius Wenzel2000-04-03
* removed 'variables';Gravatar Makarius Wenzel2000-03-27
* Attempt to fix filename mess for Windows.Gravatar David Aspinall2000-03-24
* removed 'kill_proof';Gravatar Makarius Wenzel2000-03-23
* added 'moreover';Gravatar Makarius Wenzel2000-03-23