| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1999-10-06 | Turned off C-c C-l; fixed syntax for old result form; proof-showproof-command. | David Aspinall | |
| 1999-10-06 | thy mode binding made to match with script mode | David Aspinall | |
| 1999-10-01 | Renamed some configuration variables for uniformity, see CHANGES. | David Aspinall | |
| 1999-09-30 | replaced isa-output-font-lock-terms by isa-output-font-lock-keywords-1; | Makarius Wenzel | |
| 1999-09-30 | tuned isa-init-output-syntax-table; | Makarius Wenzel | |
| removed isa-binder-regexp (obsolete); remove isa-font-lock-terms; proper isa-output-font-lock-keywords-1; | |||
| 1999-09-29 | Enabled hack for proof-shell-leave-annotations-in-output | David Aspinall | |
| 1999-09-23 | Added setting for proof-find-theorems-command. | David Aspinall | |
| 1999-09-22 | tuned example according to Isabelle style-guide; | Makarius Wenzel | |
| 1999-09-22 | improved (?) proof-shell-proof-completed-regexp; | Makarius Wenzel | |
| 1999-09-21 | Fix for proof-shell-proof-completed-regexp | David Aspinall | |
| 1999-09-21 | Adjusted proof-shell-proof-completed-regexp to match against whole of | David Aspinall | |
| proofstate output including "No subgoals!" message. Now PG can correctly set the proof-shell-proof-completed flag. | |||
| 1999-09-13 | Cleaned up example files so all demonstrate same theorem "conj_comms". | David Aspinall | |
| Would be nice to add more theorems to compare scripts in different systems. | |||
| 1999-09-03 | added bind_thms; | Makarius Wenzel | |
| added no_qed; more tacticals; removed isa-tactics (didn't make much sense); isa-goal-command-regexp accomodates "val ... =" part; | |||
| 1999-09-03 | usage: tell PROOFGENERAL_OPTIONS; | Makarius Wenzel | |
| -u true by default; | |||
| 1999-08-29 | added ALLGOALS; | Makarius Wenzel | |
| 1999-08-25 | added qed_spec_mp; | Makarius Wenzel | |
| 1999-08-23 | Maintainer addresses | David Aspinall | |
| 1999-08-23 | fixed comment; | Makarius Wenzel | |
| 1999-08-23 | Added font-lock keywords and syntax table setup for buffers displaying | David Aspinall | |
| Isabelle output. | |||
| 1999-08-23 | Improved syntax by copying from isar-syntax.el. | David Aspinall | |
| Begun on section for Isabelle output syntax. | |||
| 1999-08-20 | Disabled binder regexp font locking | David Aspinall | |
| 1999-08-20 | eliminated superficial ';'s; | Makarius Wenzel | |
| 1999-08-20 | update by DvO; | Makarius Wenzel | |
| 1999-08-18 | proof-shell-start-goals-regexp: include \n; | Makarius Wenzel | |
| isa-init-syntax-table moved to isa-syntax.el; improved isa-update-thy-only; | |||
| 1999-08-18 | isa-init-syntax-table moved here from isa.el; | Makarius Wenzel | |
| 1999-08-18 | replaced 'ProofGeneral' by 'Proof General'; | Makarius Wenzel | |
| 1999-08-18 | obsolete; | Makarius Wenzel | |
| 1999-08-16 | obsolete, use Isabelle's native ProofGeneral.init instead; | Makarius Wenzel | |
| 1999-08-16 | proof-shell-first-special-char ?\350; | Makarius Wenzel | |
| tuned prompt; deactivated "No subgoals!"; use Isabelle's native ProofGeneral.init; proper setup for theory loader actions: better handling of multiple buffers; isa-find-and-forget does nothing; | |||
| 1999-08-06 | tuned; | Makarius Wenzel | |
| 1999-08-06 | ProofGeneral interface wrapper for Isabelle/classic | Makarius Wenzel | |
| 1999-07-03 | Removed extra parenthesis. | David Aspinall | |
| 1999-07-02 | fixed some regexp via proof-anchor-regexp; | Makarius Wenzel | |
| 1999-05-27 | renamed proof-commands-regexp to proof-indent-commands-regexp, which | Makarius Wenzel | |
| is less confusing); | |||
| 1999-02-03 | fixed syntax entry for "_" | Thomas Kleymann | |
| 1999-02-01 | Regexp bug. Use proof-string-match appropriately. | David Aspinall | |
| 1999-01-12 | Changed read-no-blanks-input to read-string, former is defunct. | David Aspinall | |
| 1998-12-18 | File sent by David von Oheimb. | David Aspinall | |
| 1998-12-15 | Docstring tweak | David Aspinall | |
| 1998-12-15 | Fixed broken check on proof-mode-hook. | David Aspinall | |
| 1998-12-15 | made many minor changes to the documentation | Thomas Kleymann | |
| 1998-12-11 | Altered behaviour to allow retraction part-way through finished scripts. | David Aspinall | |
| Previously Proof General was asked to unlock a file A.ML as soon as retraction in it happened. Now Proof General is only asked to unlock the children of A.ML, although Isabelle records the fact that A.ML has been retracted. (Which means that if A.ML is later re-linked, Proof General will correctly get told about it). | |||
| 1998-12-10 | Fix for splash hack for theory files when proo-splash-inhibit=t. | David Aspinall | |
| 1998-11-26 | Added clear-goals-buffer stuff, asked for response to be left after use_thy. | David Aspinall | |
| 1998-11-25 | Cleaned up, and made use_thy remove ML file from DB properly; | David Aspinall | |
| optimised use_thy to report only on files newly added to db. | |||
| 1998-11-25 | Documentation improvements. | David Aspinall | |
| 1998-11-25 | FSF Emacs fix for buffer-file-truename, which is the | David Aspinall | |
| *abbreviated* form of file-truename! | |||
| 1998-11-25 | Fixed show_context | David Aspinall | |
| 1998-11-25 | Fixes to debug long standing not-showing-first-goal problem. | David Aspinall | |
| 1998-11-25 | Added Isamode-like keybinding C-c C-l for proof-prf. | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |