proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	handle relative heap paths gracefully;	Makarius Wenzel	2001-08-31
\|
*	back to official Isabelle99-2 (later Isabelle dists will provide	Makarius Wenzel	2001-08-31
\| \| \| \|	their own copy of this file);
*	Improved explanation	David Aspinall	2001-08-31
\|
*	Something about dependencies feature	David Aspinall	2001-08-31
\|
*	Added note about dependency feature.	David Aspinall	2001-08-31
\|
*	(Almost) complete rewrite	David Aspinall	2001-08-31
\|
*	Updated	David Aspinall	2001-08-31
\|
*	Move theorem dependency code into proof-depends.el.	David Aspinall	2001-08-31
\| \| \| \| \| \| \|	Added 'controlspan property to proof body spans: action will be controlled from the control span. (The 'goalsave is the parent). Replace 'highlight face with 'proof-mouse-highlight-face throughout.
*	Added copy command, call to dependency menu if proof-depends is loaded.	David Aspinall	2001-08-31
\|
*	Add simulations of more qed commands, also sort and uniquify dependencies.	David Aspinall	2001-08-31
\|
*	Add new proof-mouse-highlight-face to use instead of default. Fix ↵	David Aspinall	2001-08-31
\| \| \| \|	dependency faces.
*	new commands (proof terms, code generator);	Makarius Wenzel	2001-08-31
\|
*	Remove duplicate entries	David Aspinall	2001-08-31
\|
*	Add faces for theorem dependencies.	David Aspinall	2001-08-31
\|
*	Explanation	David Aspinall	2001-08-31
\|
*	Add DvO to list	David Aspinall	2001-08-31
\|
*	Add Christophe to list	David Aspinall	2001-08-31
\|
*	Add auto-compile-vos experimental setting for automatic multiple files.	David Aspinall	2001-08-31
\|
*	Remove minibuffer bug	David Aspinall	2001-08-31
\|
*	Fix for names of functions in proof-depends	David Aspinall	2001-08-31
\|
*	Add setting for turning on theorem dependency tracking	David Aspinall	2001-08-31
\|
*	Update for Isabelle99-2	David Aspinall	2001-08-31
\|
*	Clean up of proof-depends	David Aspinall	2001-08-31
\|
*	Skip settings which have no PA command in proof-assistant-settings-cmd	David Aspinall	2001-08-31
\|
*	Add proof-shell-kill-function-hooks	David Aspinall	2001-08-31
\|
*	include ISABELLE_HOME_USER/etc/isar-keywords.el or	Makarius Wenzel	2001-08-30
\| \| \| \|	ISABELLE_HOME/etc/isar-keywords.el if available;
*	updated;	Makarius Wenzel	2001-08-30
\|
*	pg-add-proof-element: removed accidential (?) dynamic scoping on	Makarius Wenzel	2001-08-30
\| \| \| \| \|	proofbodyspan; handle proof-script-integral-proofs;
*	added proof-script-integral-proofs ("Whether the complete text after a	Makarius Wenzel	2001-08-30
\| \| \| \|	goal confines the actual proof.");
*	proof-script-integral-proofs t;	Makarius Wenzel	2001-08-30
\|
*	Updated.	David Aspinall	2001-08-30
\|
*	Clarify 6.3.1 for multi file	David Aspinall	2001-08-30
\|
*	Fix interrupt hook for PolyML 4 in recent Isabelle	David Aspinall	2001-08-30
\|
*	Set version tag for new release.	David Aspinall	2001-08-30
\|
*	Add reassurance to interrupt warning to make Markus happier.	David Aspinall	2001-08-30
\|
*	Note about XEmacs 21 and x-symbol	David Aspinall	2001-08-30
\|
*	Set proof-shell-pre-interrupt-hook for PolyML (not just PolyML 3).	David Aspinall	2001-08-30
\|
*	More about invisible proofs and multiple files in Coq. X-symbol compat	David Aspinall	2001-08-30
\|
*	Updates for recent version of X-symbol, which has no file called ↵	David Aspinall	2001-08-30
\| \| \| \|	x-symbol-autoloads.
*	Add :eval form for defpacustom to define PA-specific PG settings as well as ↵	David Aspinall	2001-08-30
\| \| \| \|	PA settings.
*	Add variable proof-previous-script-buffer	David Aspinall	2001-08-30
\|
*	fixes for FSF Emacs for searching for goal span (don't call goal-command-p ↵	David Aspinall	2001-08-30
\| \| \| \|	on empty string). Fix bug in add-proof-element for disappearing proofs setting. Add setting of proof-previous-script-buffer when scripting deactivated
*	Added implementation of remassq for FSF Emacs	David Aspinall	2001-08-30
\|
*	pg-insert-last-output-as-comment strips special annotations from last output ↵	David Aspinall	2001-08-30
\| \| \| \|	before inserting as comment.
*	Fix web page for kit	David Aspinall	2001-08-28
\|
*	added something in the doc about coq-version-is-V7.	Pierre Courtieu	2001-08-28
\|
*	Added something in the doc about coq-version-is-V7, and made the setting of	Pierre Courtieu	2001-08-28
\| \| \| \|	this variable more trustable with (concat coq-prog-name "-v").
*	Updated.	David Aspinall	2001-08-28
\|
*	Set version tag for new release.	David Aspinall	2001-08-28
\|
*	Change of proof span type back to goalsave fix	David Aspinall	2001-08-28
\|