proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Added lego-global-p as always false, but for consistency with Coq mode.	Healfdene Goguen	1997-11-20
\| \| \| \|	Changed [meta (control i)] to [meta tab] in key definition.
*	Added indentation for lego-mode.	Dilip Sequiera	1997-11-18
\|
*	Added some magic commands: proof-frob-locked-end, proof-try-command,	Dilip Sequiera	1997-11-17
\| \| \| \| \|	proof-interrupt-process. Added moving nested lemmas above goal for coq. Changed the key mapping for assert-until-point to C-c RET.
*	Assign new variable proof-goal-hyp-fn to lego-goal-hyp, which is	Healfdene Goguen	1997-11-06
\| \| \| \|	simply old code for picking up goal or hypothesis for pbp
*	New indentation for lego-count-undos (smile)	Healfdene Goguen	1997-10-24
\|
*	o merged script management (1.20.2.11) on the main branch	Thomas Kleymann	1997-10-16
\| \| \| \|	o fixed a bug in lego-find-and-forget due to new treatment of comments
*	lego-count-undos is now aware that comments are treated separately	Thomas Kleymann	1997-10-13
\|
*	* empty log message *	Healfdene Goguen	1997-10-08
\|
*	minor change in font-lock pattern	Thomas Kleymann	1997-08-25
\|
*	removed font-lock support for Error messages; this is now supported in	Thomas Kleymann	1996-12-12
\| \| \| \|	the pbp package
*	Speeded up proof-by-pointing things	Dilip Sequiera	1996-12-09
\|
*	added font-lock properties for pbp-lego-mode	Thomas Kleymann	1996-12-05
\|
*	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-12-03
\|
*	o added logical macros as keywords	Thomas Kleymann	1996-11-29
\| \| \| \| \|	o removed keywords SaveFrozen and SaveUnfrozen o fixed bug in lego-outline-regexp
*	* empty log message *	Thomas Kleymann	1996-11-22
\|
*	* empty log message *	Thomas Kleymann	1996-11-21
\|
*	Cleaned ext.el up a bit in terms of its namespace and the management of	Dilip Sequiera	1996-11-17
\| \| \| \|	the comint filter.
*	minor changes regarding regular expressions	Thomas Kleymann	1996-11-13
\|
*	Fixed parenthesis matching to deal with comments	Dilip Sequiera	1996-11-13
\|
*	Yves Bertot's proof by pointing	Thomas Kleymann	1996-11-13
\|
*	improved lego-outline-regexp	Thomas Kleymann	1996-11-12
\|
*	fix for incorrect lego-outline-regexp	Thomas Kleymann	1996-11-10
\|
*	fixed bug in ids-to-regexp and improved regular expression for fontifying LEGO	Thomas Kleymann	1996-11-05
\|
*	minor bug fix wrt to font-lock regexps	Thomas Kleymann	1996-11-02
\|
*	improved font-lock customisation for LEGO	Thomas Kleymann	1996-11-01
\|
*	Fixed some bugs. Doubtless introduced others.	Dilip Sequiera	1996-10-29
\|
*	added proof-find-end-of-command	Thomas Kleymann	1996-10-25
\| \| \| \|	moved some bindings from lego-mode-map to proof-mode-map
*	Emacs mode for lego	lego	1996-10-24