proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Rename [proof]find-theorems -> isar-find-theorems	David Aspinall	2007-05-11
\|
*	Renamed file	David Aspinall	2007-05-11
\|
*	Add experimental find theorems form (not working on all Emacs yet)	David Aspinall	2007-05-10
\|
*	New files.	David Aspinall	2007-05-10
\|
*	x-symbol-isabelle-font-lock-regexp: demand subsequent non-space character;	Makarius Wenzel	2007-05-08
\|
*	undo: removed confusing comment;	Makarius Wenzel	2007-05-08
\|
*	tuned cannot-undo;	Makarius Wenzel	2007-05-08
\|
*	added isar-cmd-sledgehammer;	Makarius Wenzel	2007-05-08
\|
*	tuned pg-special-char-regexp;	Makarius Wenzel	2007-05-08
\|
*	Patch for XEmacs 21.5 beta match-replace bug	David Aspinall	2007-03-03
\|
*	Fix comment	David Aspinall	2007-02-28
\|
*	Comment about undo; use	David Aspinall	2007-01-10
\|
*	tuned;	Makarius Wenzel	2006-12-30
\|
*	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;
*	X-Symbol config. Moved from isa/	David Aspinall	2006-12-05
\|
*	Use Isar-specific isabelle-system file	David Aspinall	2006-12-05
\|
*	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
\|
*	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;
*	isar-goals-font-lock-keywords: added abbreviations;	Makarius Wenzel	2006-08-16
\|
*	Changed the type of proof-goal-command-p. It takes now a span, which	Pierre Courtieu	2006-04-26
\| \| \| \| \| \|	allows using a span attribute to detect goal commands. I think I modified all modes accordingly.
*	isar-preprocessing: replace \n by \<^newline>;	Makarius Wenzel	2006-02-12
\|
*	isar-goals-font-lock-keywords: "abbreviations";	Makarius Wenzel	2006-02-10
\|
*	old specials are recogized again;	Makarius Wenzel	2005-09-28
\|
*	updated from pre-Isabelle2005;	Makarius Wenzel	2005-09-22
\|
*	Updated.	David Aspinall	2005-09-21
\|
*	New files.	David Aspinall	2005-09-21
\|
*	Tweak.	David Aspinall	2005-09-21
\|
*	Add command menu	David Aspinall	2005-09-21
\|
*	back to xemacs as default;	Makarius Wenzel	2005-09-21
\|
*	update examples for Isabelle2005;	Makarius Wenzel	2005-09-17
\|
*	proof-shell-wakeup-char ?\^A	Makarius Wenzel	2005-09-17
\|
*	removed 8bit special chars for isar;	Makarius Wenzel	2005-09-14
\| \| \| \| \|	removed unused Pbp setup; removed 'isabelle-convert-idmarkup-to-subterm, which expects 8bit specials;
*	removed 8bit special chars for isar;	Makarius Wenzel	2005-09-14
\|
*	added option -U: Unicode (UTF-8) communication;	Makarius Wenzel	2005-09-14
\|
*	tuned isar-goals-font-lock-keywords;	Makarius Wenzel	2005-09-13
\|
*	tuned isar-keywords-theory-enclose;	Makarius Wenzel	2005-09-06
\|
*	renamed thms_containing to find_theorems;	Makarius Wenzel	2005-09-01
\|
*	special regexps: include PGASCII version;	Makarius Wenzel	2005-09-01
\| \| \| \|	pg-after-fontify-output-hook: always do pg-remove-specials;
*	special regexps: include PGASCII version;	Makarius Wenzel	2005-09-01
\|
*	tuned ML code for manipulating print_mode;	Makarius Wenzel	2005-09-01
\|
*	prefer emacs over xemacs, which rarely works out of the box;	Makarius Wenzel	2005-08-30
\|
*	added isar-font-lock-local: \<^loc> (needs x-symbol setup for x-invisible-face);	Makarius Wenzel	2005-08-26
\|
*	proof-defshortcut isar-local: \<^loc>;	Makarius Wenzel	2005-08-26
\|