| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1998-09-02 | Added make-ready for distribtion item. (2h, da) | David Aspinall | |
| 1998-09-02 | This commit was generated by cvs2git to track changes on a CVS vendor | David Aspinall | |
| branch. | |||
| 1998-09-02 | X-Symbol version 4.45 beta | David Aspinall | |
| 1998-09-01 | integrated comments following 1 Sep 98 discussion with Dave Aspinall | Thomas Kleymann | |
| on design principles in light of an Emacs mode for Isabelle | |||
| 1998-08-27 | todo | David Aspinall | |
| 1998-08-26 | proof is now able to inherit append-element from tl-list | Thomas Kleymann | |
| 1998-08-25 | X-Symbol version 4.45 beta | David Aspinall | |
| 1998-08-25 | This commit was generated by cvs2git to track changes on a CVS vendor | David Aspinall | |
| branch. | |||
| 1998-08-25 | Added further documentation. | Thomas Kleymann | |
| 1998-08-24 | X-Symbol version 4.45 beta | David Aspinall | |
| 1998-08-24 | This commit was generated by cvs2git to track changes on a CVS vendor | David Aspinall | |
| branch. | |||
| 1998-08-21 | First attempt, proof state works. | David Aspinall | |
| 1998-08-21 | Added comments. Made wakeup-char an option. | David Aspinall | |
| 1998-08-21 | Typos and fixes in Walkthrough section. | David Aspinall | |
| 1998-08-21 | Info file is easily generated from texinfo, so doesn't belong in CVS | David Aspinall | |
| 1998-08-21 | todo | David Aspinall | |
| 1998-08-14 | improved help submenu for LEGO | Thomas Kleymann | |
| - added a link to the library and the reference card for version 1.3 | |||
| 1998-08-14 | *** empty log message *** | Thomas Kleymann | |
| 1998-08-14 | *** empty log message *** | Thomas Kleymann | |
| 1998-08-14 | supports definitions of the form id == foo; | Thomas Kleymann | |
| 1998-08-11 | New branch | David Aspinall | |
| 1998-08-11 | Isabelle proof.el support. | David Aspinall | |
| 1998-08-11 | Renamed <file>-fontlock to <file>-syntax | David Aspinall | |
| 1998-08-07 | *** empty log message *** | Thomas Kleymann | |
| 1998-08-07 | o removed log entry | Thomas Kleymann | |
| o monitoring the end of imports is now implemented via a new proof-shell-process-output-system-specific hook | |||
| 1998-08-07 | o removed log entry | Thomas Kleymann | |
| o changed default for lego-tags o set up regular definitions to support definitions of the form id == term o monitoring the end of imports is now implemented via a new proof-shell-process-output-system-specific hook | |||
| 1998-08-07 | *** empty log message *** | Thomas Kleymann | |
| 1998-07-27 | Supports official LEGO release 1.3 | Thomas Kleymann | |
| 1998-06-11 | Moved proof-mode-hooks from proof-shell-config-done to | Healfdene Goguen | |
| proof-config-done. | |||
| 1998-06-11 | Added "Scheme" as definition keyword. | Healfdene Goguen | |
| 1998-06-10 | Wrote generic span functions for making spans read-only or read-write. | Healfdene Goguen | |
| Fixed bug in add-span and remove-span concerning return value of span-traverse. | |||
| 1998-06-10 | Wrote generic span functions for making spans read-only or read-write. | Healfdene Goguen | |
| 1998-06-10 | In proof-init-segmentation, only create proof-queue-span and | Healfdene Goguen | |
| proof-locked-span if they don't already exist. Call generic span function for making spans read-only. | |||
| 1998-06-10 | Compare span-end first rather than span-start in span-lt, because | Healfdene Goguen | |
| proof-lock-span is often changed and has starting point 1. Factored out common code of add-span and remove-span into span-traverse. | |||
| 1998-06-10 | Added proof-unprocessed-begin as general function to find beginning of | Healfdene Goguen | |
| unprocessed region. This should be used instead of proof-locked-end if we're not guaranteed to be in scripting buffer. proof-locked-end now calls proof-unprocessed-begin if we're in the proof-script-buffer. We set the goal name to "Unnamed_thm" if we can't find any other name for the theorem. proof-process-active-terminator now calls proof-unprocessed-begin. proof-shell-config-done now calls 'proof-mode-hook. | |||
| 1998-06-10 | Changed "\\s " to "\\s-" in proof-id as whitespace pattern. | Healfdene Goguen | |
| 1998-06-10 | Added lego-init-syntax-table as function to initialize syntax entries | Healfdene Goguen | |
| particular to LEGO, and call it from lego-shell-mode-config. | |||
| 1998-06-10 | Added coq-init-syntax-table as function to initialize syntax entries | Healfdene Goguen | |
| particular to coq. Changed proof-ctxt-string to "Print All". Call coq-init-syntax-table from coq-shell-mode-config. This was necessary to get prompts with "'"s in them (coming from goals with same) recognized. | |||
| 1998-06-10 | Added "Mutual Inductive" as definition keyword. | Healfdene Goguen | |
| Changed "\\s " into "\\s-" as whitespace pattern. | |||
| 1998-06-09 | o fixed bug in setting proof-queue-face on a colour terminal for GNU | Thomas Kleymann | |
| Emacs (19.34) o adjusting the directory (at least for LEGO) must not contain "~". We now expand `default-directory' before cding to it. [Under XEmacs (unlike Emacs 19.34), `default-directory' is already in expanded form.] | |||
| 1998-06-03 | Added '?'s before single characters in define-keys for emacs19, at | Healfdene Goguen | |
| Pascal Brisset's suggestion. | |||
| 1998-06-03 | Changed Compute from command to tactic. | Healfdene Goguen | |
| Added Fix, Destruct and Cofix as tactics. Added Local as goal. | |||
| 1998-06-03 | Changed last-span to before-list. | Healfdene Goguen | |
| Added definitions of foldr and foldl if they aren't already loaded. Changed definitions of add-span, remove-span and find-span-aux to be non-recursive. Removed detach-extent since this file isn't used by xemacs. Added function append-unique to avoid repetitions in list generated by spans-at-region. Changed next-span so it uses member-if. | |||
| 1998-06-03 | Added (require 'cl) for emacs19. | Healfdene Goguen | |
| 1998-06-03 | Added proof-goto-end-of-locked-interactive as old | Healfdene Goguen | |
| proof-goto-end-of-locked, and proof-goto-end-of-locked now doesn't switch buffer. Added code in proof-steal-process to handle case of stealing script management from a killed buffer. Set proof-active-buffer-fake-minor-mode to nil in proof-restart-script. | |||
| 1998-06-03 | Changed expression (>= 0 x) to its equivalent (eq x 0) | Healfdene Goguen | |
| Changed some variables to their associated constant in cases where we know they must be equal. | |||
| 1998-06-03 | Added definition of proof-commands-regexp for coq | Healfdene Goguen | |
| 1998-06-02 | Structured review now done. | Healfdene Goguen | |
| Added item that we need to write proof-retract-file. | |||
| 1998-06-02 | Corrected comment about this being for emacs19. | Healfdene Goguen | |
| 1998-06-02 | Corrected comment about this being for xemacs. | Healfdene Goguen | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |