aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
1996-11-13Yves Bertot:Thomas Kleymann
If you click on an hypothesis name or a goal name, then Emacs generates commands that are sent to lego but not stored in the script buffer. The fix I have is to replace pbp-construct-command
1996-11-13Yves Bertot's extension for proof by pointing. These should probablyThomas Kleymann
be integrated in the generic proof package.
1996-11-13Yves Bertot's proof by pointingThomas Kleymann
1996-11-12improved lego-outline-regexpThomas Kleymann
1996-11-10fix for incorrect lego-outline-regexpThomas Kleymann
1996-11-05Bug with semicolon minor mode near-fixedDilip Sequiera
1996-11-05fixed bug in ids-to-regexp and improved regular expression for fontifying LEGOThomas Kleymann
1996-11-02minor bug fix wrt to font-lock regexpsThomas Kleymann
1996-11-01improved font-lock customisation for LEGOThomas Kleymann
1996-10-29Fixed some bugs. Doubtless introduced others.Dilip Sequiera
1996-10-25added proof-find-end-of-commandThomas Kleymann
moved some bindings from lego-mode-map to proof-mode-map
1996-10-24Emacs mode for legolego
1996-03-15Version 4.5 (beta?) sent by CW, as a package distrib.David Aspinall
1996-03-15This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
branch.