Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | tuned proof-shell-error-regexp; | Makarius Wenzel | 1999-10-26 | |
| | ||||
* | isa-keywords-save: removed "result"; | Makarius Wenzel | 1999-10-26 | |
| | | | | | | isa-keywords-commands: added "ProofGeneral.repeat_undo"; added isa-keywords-proof-commands; added isa-verbatim; | |||
* | update by DvO; | Makarius Wenzel | 1999-10-22 | |
| | ||||
* | Changed name of proof-shell-cd-cmd for uniformity. | David Aspinall | 1999-10-21 | |
| | ||||
* | Add isa-shell-update-thy at the end of proof-activate-scripting-hook. | David Aspinall | 1999-10-20 | |
| | ||||
* | Added uncaught exception to error-regexp | David Aspinall | 1999-10-19 | |
| | ||||
* | Rename proof-mark-buffer-atomic->proof-complete-buffer-atomic. | David Aspinall | 1999-10-19 | |
| | ||||
* | Deactivate scripting before retracting a theory file. Fix for DvO's report. | David Aspinall | 1999-10-19 | |
| | ||||
* | Whitespace | David Aspinall | 1999-10-15 | |
| | ||||
* | let PROOFGENERAL_ASSISTANTS control isa vs. isar selection; | Makarius Wenzel | 1999-10-15 | |
| | ||||
* | Fix for state-preserving-p | David Aspinall | 1999-10-06 | |
| | ||||
* | 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. | |||
* | 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-06 | |
| | ||||
* | Renamed some configuration variables for uniformity, see CHANGES. | David Aspinall | 1999-10-01 | |
| | ||||
* | 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 | 1999-09-30 | |
| | | | | | | removed isa-binder-regexp (obsolete); remove isa-font-lock-terms; proper isa-output-font-lock-keywords-1; | |||
* | Enabled hack for proof-shell-leave-annotations-in-output | David Aspinall | 1999-09-29 | |
| | ||||
* | Added setting for proof-find-theorems-command. | David Aspinall | 1999-09-23 | |
| | ||||
* | tuned example according to Isabelle style-guide; | Makarius Wenzel | 1999-09-22 | |
| | ||||
* | improved (?) proof-shell-proof-completed-regexp; | Makarius Wenzel | 1999-09-22 | |
| | ||||
* | 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 | 1999-09-21 | |
| | | | | | proofstate output including "No subgoals!" message. Now PG can correctly set the proof-shell-proof-completed flag. | |||
* | Cleaned up example files so all demonstrate same theorem "conj_comms". | David Aspinall | 1999-09-13 | |
| | | | | | Would be nice to add more theorems to compare scripts in different systems. | |||
* | added bind_thms; | Makarius Wenzel | 1999-09-03 | |
| | | | | | | | added no_qed; more tacticals; removed isa-tactics (didn't make much sense); isa-goal-command-regexp accomodates "val ... =" part; | |||
* | usage: tell PROOFGENERAL_OPTIONS; | Makarius Wenzel | 1999-09-03 | |
| | | | | -u true by default; | |||
* | added ALLGOALS; | Makarius Wenzel | 1999-08-29 | |
| | ||||
* | added qed_spec_mp; | Makarius Wenzel | 1999-08-25 | |
| | ||||
* | 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 | 1999-08-23 | |
| | | | | Isabelle output. | |||
* | Improved syntax by copying from isar-syntax.el. | David Aspinall | 1999-08-23 | |
| | | | | Begun on section for Isabelle output syntax. | |||
* | 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-20 | |
| | ||||
* | proof-shell-start-goals-regexp: include \n; | Makarius Wenzel | 1999-08-18 | |
| | | | | | isa-init-syntax-table moved to isa-syntax.el; improved isa-update-thy-only; | |||
* | 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-18 | |
| | ||||
* | obsolete, use Isabelle's native ProofGeneral.init instead; | Makarius Wenzel | 1999-08-16 | |
| | ||||
* | proof-shell-first-special-char ?\350; | Makarius Wenzel | 1999-08-16 | |
| | | | | | | | | 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; | |||
* | tuned; | Makarius Wenzel | 1999-08-06 | |
| | ||||
* | ProofGeneral interface wrapper for Isabelle/classic | Makarius Wenzel | 1999-08-06 | |
| | ||||
* | Removed extra parenthesis. | David Aspinall | 1999-07-03 | |
| | ||||
* | fixed some regexp via proof-anchor-regexp; | Makarius Wenzel | 1999-07-02 | |
| | ||||
* | renamed proof-commands-regexp to proof-indent-commands-regexp, which | Makarius Wenzel | 1999-05-27 | |
| | | | | is less confusing); | |||
* | fixed syntax entry for "_" | Thomas Kleymann | 1999-02-03 | |
| | ||||
* | Regexp bug. Use proof-string-match appropriately. | David Aspinall | 1999-02-01 | |
| | ||||
* | Changed read-no-blanks-input to read-string, former is defunct. | David Aspinall | 1999-01-12 | |
| | ||||
* | File sent by David von Oheimb. | David Aspinall | 1998-12-18 | |
| |