proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Isabelle/Isar keyword classification (used to be in isar-syntax.el);	Makarius Wenzel	1999-05-23
\|
*	tuned usage;	Makarius Wenzel	1999-05-23
\| \| \| \|	do not append '/' to PROOFGENERAL_HOME;
*	tuned;	Makarius Wenzel	1999-05-21
\| \| \| \|	improved isar-find-and-forget;
*	tuned -- still quite unsatisfactory;	Makarius Wenzel	1999-05-21
\|
*	made part of the Isabelle sources;	Makarius Wenzel	1999-05-21
\|
*	I've added the custom option 'prog-name-guess' in the generic part and	Patrick Loiseleur	1999-05-17
\| \| \| \| \| \| \| \| \|	the function coq-guess-command-line in the coq part. Every prover should have the functon *-guess-command-line that uses, for example, the output of "make -n" to guess the correct command line options of the prover. Patrick
*	several additions, as usual	Patrick Loiseleur	1999-05-17
\|
*	changed use of proof-send (OLD) to proof-shell-insert	Paul Callaghan	1999-05-12
\|
*	instantiation for "plastic" proof assistant	Paul Callaghan	1999-05-11
\| \| \| \|	based on the lego instantiation.
*	added proof system "plastic", triggered by a .lf extension	Paul Callaghan	1999-05-11
\|
*	Add toggle for proof toolbar to menu	David Aspinall	1999-05-11
\|
*	todo for reorganizing menus.	David Aspinall	1999-05-11
\|
*	* empty log message *	Patrick Loiseleur	1999-05-03
\|
*	OrElse -> Orelse	Patrick Loiseleur	1999-05-03
\|
*	proof-home-directory is correct even if $PROOFGENERAL_HOME does not	Patrick Loiseleur	1999-05-03
\| \| \| \| \|	end with a slash. Moreover, the closure proof-home-directory-fn is added so that this value is not computed at compilation time.
*	proof-list-global is disabled (must be rewritten)	Patrick Loiseleur	1999-05-03
\|
*	fixed proof-shell-quit-cmd;	Makarius Wenzel	1999-04-27
\|
*	deactivated '.' and '..' keywords (tmp);	Makarius Wenzel	1999-04-27
\|
*	added "thus", "hence";	Makarius Wenzel	1999-04-23
\| \| \| \|	tuned "next";
*	Added the correct proof-shell-restart-cmd	Patrick Loiseleur	1999-04-20
\|
*	A few coloring tricks	Patrick Loiseleur	1999-04-20
\|
*	initial version of 'isar proof assistant (Isabelle/Isar);	Makarius Wenzel	1999-04-16
\|
*	added 'isar proof assistant;	Makarius Wenzel	1999-04-16
\|
*	Set version tag for new release.	proofgen	1999-04-07
\|
*	Merged changes sent by Patrick Loiseleur.	David Aspinall	1999-04-07
\|
*	Fixed.	David Aspinall	1999-03-08
\|
*	Clarification on isa-thy fix.	David Aspinall	1999-03-08
\|
*	Idea for proof-auto-retract, notes about proof-strict-read-only	David Aspinall	1999-03-08
\|
*	Improved documentation on tags	Thomas Kleymann	1999-02-24
\| \| \| \| \|	o added a suggestion by hht o documentation now at generic level only
*	extended section on Coq tags	Thomas Kleymann	1999-02-23
\|
*	Set version tag for new release.	David Aspinall	1999-02-22
\|
*	Comments from Healf explaining need for coq-goal-command-p	David Aspinall	1999-02-22
\|
*	Updated. Explained Coq syntax prob for proof-goal-command-p	David Aspinall	1999-02-22
\|
*	Mentioned PROOFGENERAL_ASSISTANTS	David Aspinall	1999-02-22
\|
*	Coq section on tags improved to mention coqtags.	David Aspinall	1999-02-22
\|
*	Coq proof mode renamed Coq Proof General	David Aspinall	1999-02-22
\|
*	Fixed for dvips which sends to printer by default.	David Aspinall	1999-02-22
\|
*	Docstring	David Aspinall	1999-02-22
\|
*	Added hack to fix nested @samp @var problem.	David Aspinall	1999-02-22
\|
*	Added PROOFGENERAL_ASSISTANTS. proof-site should not need to be edited.	David Aspinall	1999-02-22
\|
*	Updated.	David Aspinall	1999-02-22
\|
*	Fixed bug by shifting configuration of minor mode for active terminator.	David Aspinall	1999-02-22
\|
*	Updated magic. Shorted section name.	David Aspinall	1999-02-22
\|
*	Added revised version of text from Healf for Coq. Updated version ↵	David Aspinall	1999-02-22
\| \| \| \|	numbers/authors.
*	fixed syntax entry for "_"	Thomas Kleymann	1999-02-03
\|
*	Set version tag for new release.	David Aspinall	1999-02-01
\|
*	Idea to have a mailing list for PG.	David Aspinall	1999-02-01
\|
*	Regexp bug. Use proof-string-match appropriately.	David Aspinall	1999-02-01
\|
*	Improved docstring	David Aspinall	1999-02-01
\|
*	Fixed matching. Added todo for making some code more generic.	David Aspinall	1999-02-01
\|