Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | added 'case', 'print_cases'; | Makarius Wenzel | 2000-03-09 |
| | |||
* | Split low-level todo into several files. | David Aspinall | 2000-03-08 |
| | |||
* | tuned electric-ignore; | Makarius Wenzel | 2000-02-23 |
| | |||
* | fix electric-ignore (due to DvO); | Makarius Wenzel | 2000-02-15 |
| | |||
* | isar-tac-regexp: 'font-lock-reference-face; | Makarius Wenzel | 2000-02-14 |
| | |||
* | removed then_apply; | Makarius Wenzel | 2000-02-14 |
| | | | | added apply_end; | ||
* | option -x: enable x-symbol package; | Makarius Wenzel | 2000-02-11 |
| | |||
* | added "judgment"; | Makarius Wenzel | 2000-02-11 |
| | |||
* | setup proof-shell-pre-interrupt-hook for Poly/ML; | Makarius Wenzel | 2000-02-10 |
| | |||
* | tuned indentation code; | Makarius Wenzel | 2000-02-09 |
| | |||
* | added isar-keywords-qed-global, isar-global-save-command-regexp; | Makarius Wenzel | 2000-02-09 |
| | | | | | added isar-keywords-indent-reset; tuned font-lock; | ||
* | added 'oops'; | Makarius Wenzel | 2000-02-09 |
| | |||
* | added prefer, defer; | Makarius Wenzel | 2000-01-28 |
| | |||
* | Fixes for short output duplication problem: set ↵ | David Aspinall | 2000-01-06 |
| | | | | proof-shell-eager-annotation-start-length. | ||
* | added "where"; | Makarius Wenzel | 2000-01-06 |
| | |||
* | fixed isar-keywords-local-goal-regexp; | Makarius Wenzel | 1999-12-30 |
| | |||
* | tuned faces; | Makarius Wenzel | 1999-11-22 |
| | |||
* | Typo. | David Aspinall | 1999-11-18 |
| | |||
* | cleaned; | Makarius Wenzel | 1999-11-17 |
| | |||
* | Comment out some obsolete/unecessary stuff. Add X-Symbol support | David Aspinall | 1999-11-17 |
| | |||
* | Support for X-Symbol | David Aspinall | 1999-11-17 |
| | |||
* | fixed indentation bug: use proof-looking-at (proof-case-fold-search); | Makarius Wenzel | 1999-11-10 |
| | |||
* | improved proof-shell-error-regexp; | Makarius Wenzel | 1999-10-29 |
| | |||
* | (try_)context_thy_only; | Makarius Wenzel | 1999-10-27 |
| | |||
* | tuned proof-shell-error-regexp; | Makarius Wenzel | 1999-10-26 |
| | |||
* | ProofGeneral.kill_proof: clears goals buffer; | Makarius Wenzel | 1999-10-26 |
| | | | | | | ProofGeneral.restart; ProofGeneral.inform_file_processed/retracted; improved proof-shell-compute-new-files-list (more robust); | ||
* | replaced remove_thy by kill_thy (more robust); | Makarius Wenzel | 1999-10-26 |
| | |||
* | added kill_thy, touch_child_thys; | Makarius Wenzel | 1999-10-26 |
| | | | | internal ProofGeneral commands; | ||
* | isar-remove-file: compare basenames only; | Makarius Wenzel | 1999-10-22 |
| | |||
* | Changed name of proof-shell-cd-cmd for uniformity. | David Aspinall | 1999-10-21 |
| | |||
* | theory loader actions now that of PG/isa; | Makarius Wenzel | 1999-10-20 |
| | |||
* | added ML_command; | Makarius Wenzel | 1999-10-20 |
| | |||
* | added isar-detect-header; | Makarius Wenzel | 1999-10-19 |
| | | | | tuned; | ||
* | Rename proof-mark-buffer-atomic->proof-complete-buffer-atomic. | David Aspinall | 1999-10-19 |
| | |||
* | let PROOFGENERAL_ASSISTANTS control isa vs. isar selection; | Makarius Wenzel | 1999-10-15 |
| | |||
* | renamed verbatim/verb to text_raw/txt_raw; | Makarius Wenzel | 1999-10-14 |
| | |||
* | proof-shell-cd: isar-verbatim no longer required; | Makarius Wenzel | 1999-10-07 |
| | |||
* | replaced "clear_undo" to "clear_undos"; | Makarius Wenzel | 1999-10-07 |
| | | | | | replaced "title" by "header"; added "verbatim", "verb"; | ||
* | Made new command proof-cd to cd to the directory of the current | David Aspinall | 1999-10-06 |
| | | | | | | buffer. Added a version of it to proof-activate-scripting-hook. Removed cd from initialization sequence. Changed prover specifics accordingly. | ||
* | Fixed proof-showproof-command | David Aspinall | 1999-10-06 |
| | |||
* | isar-keywords-proof-asm-goal; | Makarius Wenzel | 1999-10-01 |
| | |||
* | Renamed some configuration variables for uniformity, see CHANGES. | David Aspinall | 1999-10-01 |
| | |||
* | replaced isar-output-font-lock-terms by isar-output-font-lock-keywords-1; | Makarius Wenzel | 1999-09-30 |
| | |||
* | proof-find-theorems-command "thms_containing %s;"; | Makarius Wenzel | 1999-09-30 |
| | | | | | proof-shell-leave-annotations-in-output t; replaced isar-output-font-lock-terms by isar-output-font-lock-keywords-1; | ||
* | added isar-verbatim; | Makarius Wenzel | 1999-09-26 |
| | |||
* | added thms_containing, ML_setup; | Makarius Wenzel | 1999-09-26 |
| | |||
* | proof-shell-proof-completed-regexp nil; | Makarius Wenzel | 1999-09-25 |
| | |||
* | Isabelle term / type hiliting; | Makarius Wenzel | 1999-09-24 |
| | |||
* | tuned; | Makarius Wenzel | 1999-09-24 |
| | |||
* | unified example with other proof assistants; | Makarius Wenzel | 1999-09-24 |
| |