proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Renamed <file>-fontlock to <file>-syntax	David Aspinall	1998-08-11
\|
*	Added "Scheme" as definition keyword.	Healfdene Goguen	1998-06-11
\|
*	Added "Mutual Inductive" as definition keyword.	Healfdene Goguen	1998-06-10
\| \| \| \|	Changed "\\s " into "\\s-" as whitespace pattern.
*	Changed Compute from command to tactic.	Healfdene Goguen	1998-06-03
\| \| \| \| \|	Added Fix, Destruct and Cofix as tactics. Added Local as goal.
*	Minor modifications to comments	Healfdene Goguen	1998-06-02
\|
*	Added CoFixpoint and tactics.	Healfdene Goguen	1998-05-15
\| \| \| \|	Changed indentation.
*	Added CoInductive.	Healfdene Goguen	1998-05-05
\| \| \| \| \|	Made updates to reflect problem with "Definition", which couldn't be used with proof scripts.
*	Added coq-shell-cd	Healfdene Goguen	1998-01-15
\| \| \| \|	Some new fontlocks
*	Incorporated tms's suggestion for simplifying coq-font-lock-keywords-1	Healfdene Goguen	1997-11-26
\|
*	Updates to Coq fontlock tables	Healfdene Goguen	1997-11-06
\|
*	Updates for coq, including:	Healfdene Goguen	1997-10-30
\| \| \| \| \| \|	* pbp-goal-command and pbp-hyp-command use proof-terminal-string * updates to keywords * fix for goal regexp
*	Changed order of "Inversion_clear" and "Inversion" so that former is	Healfdene Goguen	1997-10-24
\| \| \| \| \|	fontified first. Added "Print" to list of commands.
*	Added "Induction" as tactic	Healfdene Goguen	1997-10-17
\|
*	* empty log message *	Thomas Kleymann	1997-10-13