index
:
proof-general
master
Emacs plugins for proof management systems
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
1997-10-30
Updates for coq, including:
Healfdene Goguen
1997-10-24
Updated comment about extent types
Healfdene Goguen
1997-10-24
New indentation for lego-count-undos (smile)
Healfdene Goguen
1997-10-24
Fixed coq-count-undos for comments
Healfdene Goguen
1997-10-24
Changed order of "Inversion_clear" and "Inversion" so that former is
Healfdene Goguen
1997-10-22
Updated proof-segment-up-to to take ""'s into account
Healfdene Goguen
1997-10-17
proof-active-terminator inside comment case fixed. Also maybe the
Dilip Sequiera
1997-10-17
Fixed coq-shell-prompt-pattern to reflect proof-id
Healfdene Goguen
1997-10-17
Added "Induction" as tactic
Healfdene Goguen
1997-10-17
fixed a bug in proof-process-active-terminator. Notice that it still
Thomas Kleymann
1997-10-16
Figured out display tables.
Dilip Sequiera
1997-10-16
Merged Coq changes with main branch.
Dilip Sequiera
1997-10-16
Merged Coq changes onto main branch
Dilip Sequiera
1997-10-16
merged script management (1.10.2.18) with main branch
Thomas Kleymann
1997-10-16
o merged script management (1.20.2.11) on the main branch
Thomas Kleymann
1997-10-14
proof-process-active-terminator is now an extension of
Thomas Kleymann
1997-10-13
*** empty log message ***
Thomas Kleymann
1997-10-13
put script-management branch back on main branch
Thomas Kleymann
1997-10-13
The package pbp is now integrated in the proof package
Thomas Kleymann
1997-10-13
lego-count-undos is now aware that comments are treated separately
Thomas Kleymann
1997-10-08
*** empty log message ***
Healfdene Goguen
1997-09-18
X-Symbol version 4.45 beta
David Aspinall
1997-09-18
This commit was generated by cvs2git to track changes on a CVS vendor
David Aspinall
1997-09-17
X-Symbol version 4.45 beta
David Aspinall
1997-09-17
This commit was generated by cvs2git to track changes on a CVS vendor
David Aspinall
1997-08-25
minor change in font-lock pattern
Thomas Kleymann
1997-03-06
implementation of pbptop now records if selected goal is not current,
Thomas Kleymann
1997-01-27
improved highlighting of error messages
Thomas Kleymann
1996-12-12
support for highlighting Error messages in pbp-mode without using font-lock
Thomas Kleymann
1996-12-12
removed font-lock support for Error messages; this is now supported in
Thomas Kleymann
1996-12-09
Took out some debugging code accidentally left in.
Dilip Sequiera
1996-12-09
Speeded up proof-by-pointing things
Dilip Sequiera
1996-12-05
added variable pbp-mode-is so that pbp-mode can be inherited
Thomas Kleymann
1996-12-05
added font-lock properties for pbp-lego-mode
Thomas Kleymann
1996-12-03
added pbp-mode
Thomas Kleymann
1996-12-03
Invisible pbp command handling
Dilip Sequiera
1996-12-03
minor extensions of regular expressions
Thomas Kleymann
1996-12-03
Minor fix for performance reasons.
Dilip Sequiera
1996-12-03
A few small fixes to deal with performance problems.
Dilip Sequiera
1996-11-29
removed debug information
Thomas Kleymann
1996-11-29
o added logical macros as keywords
Thomas Kleymann
1996-11-22
pbp.el succeeds ext.el
Thomas Kleymann
1996-11-22
A generic package for proof-by-pointing
Thomas Kleymann
1996-11-22
*** empty log message ***
Thomas Kleymann
1996-11-21
Synchro bug fixed.
Dilip Sequiera
1996-11-21
*** empty log message ***
Thomas Kleymann
1996-11-18
Fixed Undo problem, now prettifies output, and deals a bit more gracefully
Dilip Sequiera
1996-11-17
Cleaned ext.el up a bit in terms of its namespace and the management of
Dilip Sequiera
1996-11-13
minor changes regarding regular expressions
Thomas Kleymann
1996-11-13
Fixed parenthesis matching to deal with comments
Dilip Sequiera
[prev]
[next]