proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	Updated magic	David Aspinall	2000-08-28
\|
*	Fix recursive make	David Aspinall	2000-08-28
\|
*	Note about CVSROOT setting.	David Aspinall	2000-08-28
\|
*	Branch	David Aspinall	2000-08-28
\|
*	Remove Library.timings call, restore compatibility with I99.	David Aspinall	2000-08-28
\|
*	Branch	David Aspinall	2000-08-28
\|
*	Files for twelf, not working at all yet.	David Aspinall	2000-08-28
\|
*	Updated	David Aspinall	2000-08-28
\|
*	Added a couple of todos	David Aspinall	2000-08-28
\|
*	Change name of mode: isar-proofscript-mode -> isar-mode and remove	David Aspinall	2000-08-28
\| \| \| \| \| \| \|	alias. Regular mode name needed for fancy macros. Use proof-definvisible fancy macro to define help menu functions. Removed parentheses from menu entries so key bindings show up.
*	Missing full stop	David Aspinall	2000-08-28
\|
*	Test file for proof-shell-set-elisp-variable-regexp	David Aspinall	2000-08-28
\|
*	Added setting for proof-shell-set-elisp-variable-regexp	David Aspinall	2000-08-28
\|
*	Added proof-shell-set-elisp-variable-regexp	David Aspinall	2000-08-28
\|
*	Added twelf and experimental support note.	David Aspinall	2000-08-28
\|
*	FIXME note added, missing docstring from macro fn def.	David Aspinall	2000-08-28
\|
*	News updated	David Aspinall	2000-08-28
\|
*	Link to two manuals now.	David Aspinall	2000-08-28
\|
*	Split manual into two parts.	David Aspinall	2000-08-28
\| \| \| \| \| \| \| \| \|	Added notes about find theorems trick of separating constants by comma for Isabelle. Made for version 99-1. Improved documentation for urgent messages, including recent additions. Mentioned new high-level macros proof-defshortcut, proof-definvisible.
*	cd command: add_path;	Makarius Wenzel	2000-08-28
\|
*	conditional load of proof-site.el;	Makarius Wenzel	2000-08-28
\|
*	-w false implies -x false;	Makarius Wenzel	2000-08-28
\| \| \| \|	do not load proof-site.el here;
*	nothing important, I forgot to undo something before my last commit in	Pierre Courtieu	2000-08-26
\| \| \| \|	coq/x-symbol-coq.el
*	Some changes for undoing with coq, handle user-defined tactics, in	Pierre Courtieu	2000-08-26
\| \| \| \|	coq/coq-syntax.el and coq/coq.el.
*	more symbols;	Makarius Wenzel	2000-08-23
\|
*	tuned x-symbol setup;	Makarius Wenzel	2000-08-23
\|
*	isar-keywords-proof-improper;	Makarius Wenzel	2000-08-16
\|
*	added isar-keywords-proof-improper;	Makarius Wenzel	2000-08-16
\| \| \| \|	tuned;
*	Added Fiona's changes, cleaned up a little bit with header and footer	David Aspinall	2000-08-14
\|
*	Added split string on theorem dependency code, to make list of dependents.	David Aspinall	2000-08-14
\|
*	Added Fiona's changes, cleaned up a little bit	David Aspinall	2000-08-14
\|
*	Added Fiona's changes.	David Aspinall	2000-08-14
\|
*	Files for testing theorem dependency features.	David Aspinall	2000-08-14
\|
*	enhancement of outline regexps for coq, now when hiding bodies, we see	Pierre Courtieu	2000-08-14
\| \| \| \| \|	completely definitions and theorems, but proof script are hidden (but can be blindly sent to the prover). Seems to work correctly.
*	enhancement of x-symbol for coq, philosophy is not encoded, and phi1 is,	Pierre Courtieu	2000-08-14
\| \| \| \|	one problem remains: a word ending with phi will be encoded.
*	smart setup of X-Symbol mode;	Makarius Wenzel	2000-08-09
\|
*	Set version tag for new release.	David Aspinall	2000-08-09
\|
*	added outline mode setup (still not quite working as expected);	Makarius Wenzel	2000-08-07
\|
*	cleaned up outline stuff;	Makarius Wenzel	2000-08-07
\|
*	new category isar-keywords-proof-heading;	Makarius Wenzel	2000-08-07
\|
*	** B make help key bindings appear in "Show me ..." menu;	Makarius Wenzel	2000-08-03
\|
*	added isar-help functions / keys (how do I get keys into menus?);	Makarius Wenzel	2000-08-03
\|
*	x-symbol-isabelle-electric-ignore: include [[ ]];	Makarius Wenzel	2000-08-03
\|
*	handle comment inside a command (patch by da);	Makarius Wenzel	2000-08-03
\|
*	x-symbol-isabelle-prepare-table: avoids redundancy in code, improves	Makarius Wenzel	2000-08-02
\| \| \| \|	on isar version (only 1 backslash);
*	tuned;	Makarius Wenzel	2000-08-02
\|
*	added isa-preprocessing;	Makarius Wenzel	2000-08-02
\|
*	fixed isar-goals-font-lock-keywords;	Makarius Wenzel	2000-07-29
\|
*	added "thm_deps", "overloaded";	Makarius Wenzel	2000-07-29
\|
*	updated;	Makarius Wenzel	2000-07-26
\|