aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
1998-09-08Added FIXMEs.David Aspinall
Added documentation. proof-segment-up-to: Removed explicit ML-style comment syntax, added END-OF-COMMAND argument. proof-undo-last-successful-command: Added optional argument to not delete. (The difference between this and proof-retract-until-point is that it infers the last command). proof-assert-next-command: Experimental alternative to proof-assert-until-point to match undo-last-successful-command.
1998-09-08Added Id and commentsDavid Aspinall
1998-09-08Added IdDavid Aspinall
1998-09-08Some quickly hacked ugly icons.David Aspinall
1998-09-08First version of generic proof toolbar.David Aspinall
1998-09-08Made customize variables user-visibleDavid Aspinall
1998-09-08Added image directory for toolbar iconsDavid Aspinall
1998-09-08More features working. Added example.David Aspinall
1998-09-08Added make item to build ChangeLog automatically, removed from repositoryDavid Aspinall
1998-09-08Layout.David Aspinall
1998-09-08Added items, assigned some to daDavid Aspinall
1998-09-08Example copied from texinfo manualDavid Aspinall
1998-09-08assigned a task to tmsThomas Kleymann
1998-09-08removed dependency on tl-listThomas Kleymann
1998-09-03New file.David Aspinall
1998-09-03Renamed/added defcustom support.David Aspinall
1998-09-03Added some defcustom supportDavid Aspinall
1998-09-03Added Isabelle example and skeleton for Coq and Lego.David Aspinall
1998-09-03A 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-03Requires proof-site.David Aspinall
1998-09-03Site-wide configuration for proof mode.David Aspinall
1998-09-03Requirement for test script addedDavid Aspinall
1998-09-03Began notes at end about adding new assistant supportDavid Aspinall
1998-09-03Renamed texinfo file.David Aspinall
1998-09-03Renamed for new subdirectory structureDavid Aspinall
1998-09-03minor modificationsThomas Kleymann
1998-09-03Dead code.David Aspinall
1998-09-03Added some items.David Aspinall
1998-09-03Removed dead codeDavid Aspinall
1998-09-03Added note of what to do here.David Aspinall
1998-09-03Added more items.David Aspinall
1998-09-03Reorganization and fixes.David Aspinall
1998-09-03Added some documentation. Fixed a bug: indent-line-function needsDavid Aspinall
to be made into a local variable.
1998-09-02o rearranged Release entryThomas Kleymann
o allocated a task to tms
1998-09-02Added make-ready for distribtion item. (2h, da)David Aspinall
1998-09-02This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
branch.
1998-09-02X-Symbol version 4.45 betaDavid Aspinall
1998-09-01integrated comments following 1 Sep 98 discussion with Dave AspinallThomas Kleymann
on design principles in light of an Emacs mode for Isabelle
1998-08-27todoDavid Aspinall
1998-08-26proof is now able to inherit append-element from tl-listThomas Kleymann
1998-08-25X-Symbol version 4.45 betaDavid Aspinall
1998-08-25This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
branch.
1998-08-25Added further documentation.Thomas Kleymann
1998-08-24X-Symbol version 4.45 betaDavid Aspinall
1998-08-24This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
branch.
1998-08-21First attempt, proof state works.David Aspinall
1998-08-21Added comments. Made wakeup-char an option.David Aspinall
1998-08-21Typos and fixes in Walkthrough section.David Aspinall
1998-08-21Info file is easily generated from texinfo, so doesn't belong in CVSDavid Aspinall
1998-08-21todoDavid Aspinall
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 01:07:59 +0000