| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 1998-09-08 | assigned a task to tms | Thomas Kleymann | |
| 1998-09-03 | A Sometimes e.g., ~tms/lego/imperative/recursion/Prepare_vc.l, | Thomas Kleymann | |
| annotations are recorded in the object file. This needs to be changed in the SML code. (initially 2h tms) Done. :-) | |||
| 1998-09-03 | Requirement for test script added | David Aspinall | |
| 1998-09-03 | Dead code. | David Aspinall | |
| 1998-09-03 | Added some items. | David Aspinall | |
| 1998-09-03 | Added more items. | David Aspinall | |
| 1998-09-02 | o rearranged Release entry | Thomas Kleymann | |
| o allocated a task to tms | |||
| 1998-09-02 | Added make-ready for distribtion item. (2h, da) | 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-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-07 | *** empty log message *** | Thomas Kleymann | |
| 1998-06-02 | Structured review now done. | Healfdene Goguen | |
| Added item that we need to write proof-retract-file. | |||
| 1998-05-29 | o outsourced indentation to proof-indent | Thomas Kleymann | |
| o support indentation of commands o replaced test of Emacs version with availability test of specific features o C-c C-c, C-c C-v and M-tab is now available in all buffers | |||
| 1998-05-26 | Necessary changes for emacs19 version | Healfdene Goguen | |
| 1998-05-21 | Changing buffers now works. | Healfdene Goguen | |
| 1998-05-21 | Fixed lifting globals. | Healfdene Goguen | |
| Added problem of buffers and need for incremental adding of tactics in Coq. | |||
| 1998-05-19 | Removed indentation problem. | Healfdene Goguen | |
| Added comments about current state of emacs19 port. | |||
| 1998-05-16 | *** empty log message *** | Thomas Kleymann | |
| 1998-05-15 | Added problem with indentation. | Healfdene Goguen | |
| 1998-05-13 | revised in light of today's meeting with hhg | Thomas Kleymann | |
| 1998-05-12 | Added documentation for C-c C-s in Coq mode. | Healfdene Goguen | |
| Fixed problem with tabbing changing buffers. | |||
| 1998-05-08 | Updated todo list. | Healfdene Goguen | |
| 1998-05-05 | Coq now restarts if going back to beginning of proof. | Healfdene Goguen | |
| 1998-02-11 | prioritised | Thomas Kleymann | |
| 1998-02-10 | *** empty log message *** | Thomas Kleymann | |
| 1998-01-15 | One needed change for coq included | Healfdene Goguen | |
| 1997-12-18 | *** empty log message *** | Thomas Kleymann | |
| 1997-11-26 | Noted bug in popup-eager-annotation | Dilip Sequiera | |
| 1997-11-26 | A few new suggestions | Healfdene Goguen | |
| 1997-11-20 | Fixed outstanding things to be updated in Coq. | Healfdene Goguen | |
| 1997-11-18 | Added indentation for lego-mode. | Dilip Sequiera | |
| 1997-11-17 | Added some magic commands: proof-frob-locked-end, proof-try-command, | Dilip Sequiera | |
| proof-interrupt-process. Added moving nested lemmas above goal for coq. Changed the key mapping for assert-until-point to C-c RET. | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |