proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	Patch for XEmacs 21.5 beta match-replace bug	David Aspinall	2007-03-03
\|
*	Remove proof-indent-pad-eol atrocity	David Aspinall	2007-02-28
\|
*	Updated.	David Aspinall	2007-02-28
\|
*	Fix comment	David Aspinall	2007-02-28
\|
*	Renamed file	David Aspinall	2007-02-28
\|
*	Note on sudo and cp -p clash	David Aspinall	2007-02-27
\|
*	Mention prefer-coding-system as suggested by Florian Haftmann	David Aspinall	2007-02-22
\|
*	New files.	David Aspinall	2007-02-08
\|
*	Patch x-symbol problem with XEmacs beta	David Aspinall	2007-01-20
\|
*	Correct mail domain	David Aspinall	2007-01-20
\|
*	Tweak.	David Aspinall	2007-01-20
\|
*	Comment about undo; use	David Aspinall	2007-01-10
\|
*	Set version tag for new release.	David Aspinall	2007-01-09
\|
*	Demonstrate faulty error reporting. Somewhat obscure, unless some	David Aspinall	2007-01-03
\| \| \| \|	tactics are using Output.error_msg rather than the "error" function.
*	Add FAQ on funny symbols/x-symbol problems	David Aspinall	2007-01-03
\|
*	Compatibility notes	David Aspinall	2007-01-03
\|
*	tuned;	Makarius Wenzel	2006-12-30
\|
*	Added some keywords ("Declare Module Import"...).	Pierre Courtieu	2006-12-22
\|
*	Remove thy-mode from isa	David Aspinall	2006-12-20
\|
*	Remove isa dir	David Aspinall	2006-12-20
\|
*	Set version tag for new release.	David Aspinall	2006-12-20
\|
*	Support older version of define-minor-mode	David Aspinall	2006-12-19
\|
*	Added completion to coq-prog-name asking.	Pierre Courtieu	2006-12-13
\|
*	Fixed keyboard shortcuts.	Pierre Courtieu	2006-12-12
\|
*	Fixed coq 8.0 compatibility and coq version detection.	Pierre Courtieu	2006-12-12
\|
*	Set version tag for new release.	David Aspinall	2006-12-11
\|
*	Update, note about Isabelle 2004	David Aspinall	2006-12-11
\|
*	back again for isar;	Makarius Wenzel	2006-12-07
\|
*	isar-keywords-theory-enclose: isar-keywords-theory-switch is back again (in ↵	Makarius Wenzel	2006-12-07
\| \| \| \|	post-Isabelle2005 the latter is empty anyway);
*	removed obsolete references to 'isa';	Makarius Wenzel	2006-12-07
\|
*	proof-shell-pre-interrupt-hook: removed obsolete Poly/ML 3 setup, which ↵	Makarius Wenzel	2006-12-07
\| \| \| \|	breaks Poly/MK 5;
*	New files.	David Aspinall	2006-12-05
\|
*	Deleted file	David Aspinall	2006-12-05
\|
*	X-Symbol config. Moved from isa/	David Aspinall	2006-12-05
\|
*	Use Isar-specific isabelle-system file	David Aspinall	2006-12-05
\|
*	Set version tag for new release.	David Aspinall	2006-11-07
\|
*	isar-keywords-theory-enclose: removed isar-keywords-theory-switch, which ↵	Makarius Wenzel	2006-11-04
\| \| \| \| \| \| \|	usually appears locally as plain theory command; isar-keywords-proper: simplified font-lock; added isar-match-nesting -- distinguishes font-lock for local vs. global begin/end;
*	isar-strip-terminators, isar-detect-begin: proof-search-forward;	Makarius Wenzel	2006-11-04
\|
*	New files.	David Aspinall	2006-10-29
\|
*	Updated.	David Aspinall	2006-10-29
\|
*	Set version tag for new release.	David Aspinall	2006-10-27
\|
*	Rationalise testing for different values of window-system, to/and support ↵	David Aspinall	2006-10-27
\| \| \| \|	more Emacs ports easily
*	Error highlighting in coq only when scripting (not when sending	Pierre Courtieu	2006-10-23
\| \| \| \|	command invisibly).
*	reintroduced pg-subterm-first-special-char, which makes PG strip goal markup;	Makarius Wenzel	2006-10-11
\| \| \| \| \|	isar-find-and-forget: no special treatment of undo-kill, allows "context" command to act as local theory init;
*	isar-keywords-indent-enclose: include "begin" keyword;	Makarius Wenzel	2006-10-11
\| \| \| \|	removed obsolete kill/undo-kill-regexp;
*	added regexps for begin/end and theory start;	Makarius Wenzel	2006-10-11
\|
*	removed obsolete isar-detect-header;	Makarius Wenzel	2006-10-11
\| \| \| \|	isar-find-and-forget: proper handling of nested begin/end blocks;
*	Fix for coq-utf-safe.	Pierre Courtieu	2006-10-06
\|
*	utf safe coq mode is not linked to proof-shell-unicode, as unicode is	Pierre Courtieu	2006-09-29
\| \| \| \|	not well handle by xemacs.
*	adapting to proof-shell-unicode. Coq has not been adapted to the	Pierre Courtieu	2006-09-29
\| \| \| \|	-emacs-U option.