aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
Commit message (Expand)AuthorAge
* Split low-level todo into several files.Gravatar David Aspinall2000-03-08
* tuned electric-ignore;Gravatar Makarius Wenzel2000-02-23
* fix electric-ignore (due to DvO);Gravatar Makarius Wenzel2000-02-15
* isar-tac-regexp: 'font-lock-reference-face;Gravatar Makarius Wenzel2000-02-14
* removed then_apply;Gravatar Makarius Wenzel2000-02-14
* option -x: enable x-symbol package;Gravatar Makarius Wenzel2000-02-11
* added "judgment";Gravatar Makarius Wenzel2000-02-11
* setup proof-shell-pre-interrupt-hook for Poly/ML;Gravatar Makarius Wenzel2000-02-10
* tuned indentation code;Gravatar Makarius Wenzel2000-02-09
* added isar-keywords-qed-global, isar-global-save-command-regexp;Gravatar Makarius Wenzel2000-02-09
* added 'oops';Gravatar Makarius Wenzel2000-02-09
* added prefer, defer;Gravatar Makarius Wenzel2000-01-28
* Fixes for short output duplication problem: set proof-shell-eager-annotation-...Gravatar David Aspinall2000-01-06
* added "where";Gravatar Makarius Wenzel2000-01-06
* fixed isar-keywords-local-goal-regexp;Gravatar Makarius Wenzel1999-12-30
* tuned faces;Gravatar Makarius Wenzel1999-11-22
* Typo.Gravatar David Aspinall1999-11-18
* cleaned;Gravatar Makarius Wenzel1999-11-17
* Comment out some obsolete/unecessary stuff. Add X-Symbol supportGravatar David Aspinall1999-11-17
* Support for X-SymbolGravatar David Aspinall1999-11-17
* fixed indentation bug: use proof-looking-at (proof-case-fold-search);Gravatar Makarius Wenzel1999-11-10
* improved proof-shell-error-regexp;Gravatar Makarius Wenzel1999-10-29
* (try_)context_thy_only;Gravatar Makarius Wenzel1999-10-27
* tuned proof-shell-error-regexp;Gravatar Makarius Wenzel1999-10-26
* ProofGeneral.kill_proof: clears goals buffer;Gravatar Makarius Wenzel1999-10-26
* replaced remove_thy by kill_thy (more robust);Gravatar Makarius Wenzel1999-10-26
* added kill_thy, touch_child_thys;Gravatar Makarius Wenzel1999-10-26
* isar-remove-file: compare basenames only;Gravatar Makarius Wenzel1999-10-22
* Changed name of proof-shell-cd-cmd for uniformity.Gravatar David Aspinall1999-10-21
* theory loader actions now that of PG/isa;Gravatar Makarius Wenzel1999-10-20
* added ML_command;Gravatar Makarius Wenzel1999-10-20
* added isar-detect-header;Gravatar Makarius Wenzel1999-10-19
* Rename proof-mark-buffer-atomic->proof-complete-buffer-atomic.Gravatar David Aspinall1999-10-19
* let PROOFGENERAL_ASSISTANTS control isa vs. isar selection;Gravatar Makarius Wenzel1999-10-15
* renamed verbatim/verb to text_raw/txt_raw;Gravatar Makarius Wenzel1999-10-14
* proof-shell-cd: isar-verbatim no longer required;Gravatar Makarius Wenzel1999-10-07
* replaced "clear_undo" to "clear_undos";Gravatar Makarius Wenzel1999-10-07
* Made new command proof-cd to cd to the directory of the currentGravatar David Aspinall1999-10-06
* Fixed proof-showproof-commandGravatar David Aspinall1999-10-06
* isar-keywords-proof-asm-goal;Gravatar Makarius Wenzel1999-10-01
* Renamed some configuration variables for uniformity, see CHANGES.Gravatar David Aspinall1999-10-01
* replaced isar-output-font-lock-terms by isar-output-font-lock-keywords-1;Gravatar Makarius Wenzel1999-09-30
* proof-find-theorems-command "thms_containing %s;";Gravatar Makarius Wenzel1999-09-30
* added isar-verbatim;Gravatar Makarius Wenzel1999-09-26
* added thms_containing, ML_setup;Gravatar Makarius Wenzel1999-09-26
* proof-shell-proof-completed-regexp nil;Gravatar Makarius Wenzel1999-09-25
* Isabelle term / type hiliting;Gravatar Makarius Wenzel1999-09-24
* tuned;Gravatar Makarius Wenzel1999-09-24
* unified example with other proof assistants;Gravatar Makarius Wenzel1999-09-24
* lemma and_comms;Gravatar Makarius Wenzel1999-09-21