aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
1997-10-30Updates for coq, including:Healfdene Goguen
1997-10-24Updated comment about extent typesHealfdene Goguen
1997-10-24New indentation for lego-count-undos (smile)Healfdene Goguen
1997-10-24Fixed coq-count-undos for commentsHealfdene Goguen
1997-10-24Changed order of "Inversion_clear" and "Inversion" so that former isHealfdene Goguen
1997-10-22Updated proof-segment-up-to to take ""'s into accountHealfdene Goguen
1997-10-17proof-active-terminator inside comment case fixed. Also maybe theDilip Sequiera
1997-10-17Fixed coq-shell-prompt-pattern to reflect proof-idHealfdene Goguen
1997-10-17Added "Induction" as tacticHealfdene Goguen
1997-10-17fixed a bug in proof-process-active-terminator. Notice that it stillThomas Kleymann
1997-10-16Figured out display tables.Dilip Sequiera
1997-10-16Merged Coq changes with main branch.Dilip Sequiera
1997-10-16Merged Coq changes onto main branchDilip Sequiera
1997-10-16merged script management (1.10.2.18) with main branchThomas Kleymann
1997-10-16o merged script management (1.20.2.11) on the main branchThomas Kleymann
1997-10-14proof-process-active-terminator is now an extension ofThomas Kleymann
1997-10-13*** empty log message ***Thomas Kleymann
1997-10-13put script-management branch back on main branchThomas Kleymann
1997-10-13The package pbp is now integrated in the proof packageThomas Kleymann
1997-10-13lego-count-undos is now aware that comments are treated separatelyThomas Kleymann
1997-10-08*** empty log message ***Healfdene Goguen
1997-09-18X-Symbol version 4.45 betaDavid Aspinall
1997-09-18This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
1997-09-17X-Symbol version 4.45 betaDavid Aspinall
1997-09-17This commit was generated by cvs2git to track changes on a CVS vendorDavid Aspinall
1997-08-25minor change in font-lock patternThomas Kleymann
1997-03-06implementation of pbptop now records if selected goal is not current,Thomas Kleymann
1997-01-27improved highlighting of error messagesThomas Kleymann
1996-12-12support for highlighting Error messages in pbp-mode without using font-lockThomas Kleymann
1996-12-12removed font-lock support for Error messages; this is now supported inThomas Kleymann
1996-12-09Took out some debugging code accidentally left in.Dilip Sequiera
1996-12-09Speeded up proof-by-pointing thingsDilip Sequiera
1996-12-05added variable pbp-mode-is so that pbp-mode can be inheritedThomas Kleymann
1996-12-05added font-lock properties for pbp-lego-modeThomas Kleymann
1996-12-03added pbp-modeThomas Kleymann
1996-12-03Invisible pbp command handlingDilip Sequiera
1996-12-03minor extensions of regular expressionsThomas Kleymann
1996-12-03Minor fix for performance reasons.Dilip Sequiera
1996-12-03A few small fixes to deal with performance problems.Dilip Sequiera
1996-11-29removed debug informationThomas Kleymann
1996-11-29o added logical macros as keywordsThomas Kleymann
1996-11-22pbp.el succeeds ext.elThomas Kleymann
1996-11-22A generic package for proof-by-pointingThomas Kleymann
1996-11-22*** empty log message ***Thomas Kleymann
1996-11-21Synchro bug fixed.Dilip Sequiera
1996-11-21*** empty log message ***Thomas Kleymann
1996-11-18Fixed Undo problem, now prettifies output, and deals a bit more gracefullyDilip Sequiera
1996-11-17Cleaned ext.el up a bit in terms of its namespace and the management ofDilip Sequiera
1996-11-13minor changes regarding regular expressionsThomas Kleymann
1996-11-13Fixed parenthesis matching to deal with commentsDilip Sequiera