proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	New/updated information files	David Aspinall	2000-03-13
\|
*	added 'case', 'print_cases';	Makarius Wenzel	2000-03-09
\|
*	Split low-level todo into several files.	David Aspinall	2000-03-08
\|
*	tuned electric-ignore;	Makarius Wenzel	2000-02-23
\|
*	fix electric-ignore (due to DvO);	Makarius Wenzel	2000-02-15
\|
*	isar-tac-regexp: 'font-lock-reference-face;	Makarius Wenzel	2000-02-14
\|
*	removed then_apply;	Makarius Wenzel	2000-02-14
\| \| \| \|	added apply_end;
*	option -x: enable x-symbol package;	Makarius Wenzel	2000-02-11
\|
*	added "judgment";	Makarius Wenzel	2000-02-11
\|
*	setup proof-shell-pre-interrupt-hook for Poly/ML;	Makarius Wenzel	2000-02-10
\|
*	tuned indentation code;	Makarius Wenzel	2000-02-09
\|
*	added isar-keywords-qed-global, isar-global-save-command-regexp;	Makarius Wenzel	2000-02-09
\| \| \| \| \|	added isar-keywords-indent-reset; tuned font-lock;
*	added 'oops';	Makarius Wenzel	2000-02-09
\|
*	added prefer, defer;	Makarius Wenzel	2000-01-28
\|
*	Fixes for short output duplication problem: set ↵	David Aspinall	2000-01-06
\| \| \| \|	proof-shell-eager-annotation-start-length.
*	added "where";	Makarius Wenzel	2000-01-06
\|
*	fixed isar-keywords-local-goal-regexp;	Makarius Wenzel	1999-12-30
\|
*	tuned faces;	Makarius Wenzel	1999-11-22
\|
*	Typo.	David Aspinall	1999-11-18
\|
*	cleaned;	Makarius Wenzel	1999-11-17
\|
*	Comment out some obsolete/unecessary stuff. Add X-Symbol support	David Aspinall	1999-11-17
\|
*	Support for X-Symbol	David Aspinall	1999-11-17
\|
*	fixed indentation bug: use proof-looking-at (proof-case-fold-search);	Makarius Wenzel	1999-11-10
\|
*	improved proof-shell-error-regexp;	Makarius Wenzel	1999-10-29
\|
*	(try_)context_thy_only;	Makarius Wenzel	1999-10-27
\|
*	tuned proof-shell-error-regexp;	Makarius Wenzel	1999-10-26
\|
*	ProofGeneral.kill_proof: clears goals buffer;	Makarius Wenzel	1999-10-26
\| \| \| \| \| \|	ProofGeneral.restart; ProofGeneral.inform_file_processed/retracted; improved proof-shell-compute-new-files-list (more robust);
*	replaced remove_thy by kill_thy (more robust);	Makarius Wenzel	1999-10-26
\|
*	added kill_thy, touch_child_thys;	Makarius Wenzel	1999-10-26
\| \| \| \|	internal ProofGeneral commands;
*	isar-remove-file: compare basenames only;	Makarius Wenzel	1999-10-22
\|
*	Changed name of proof-shell-cd-cmd for uniformity.	David Aspinall	1999-10-21
\|
*	theory loader actions now that of PG/isa;	Makarius Wenzel	1999-10-20
\|
*	added ML_command;	Makarius Wenzel	1999-10-20
\|
*	added isar-detect-header;	Makarius Wenzel	1999-10-19
\| \| \| \|	tuned;
*	Rename proof-mark-buffer-atomic->proof-complete-buffer-atomic.	David Aspinall	1999-10-19
\|
*	let PROOFGENERAL_ASSISTANTS control isa vs. isar selection;	Makarius Wenzel	1999-10-15
\|
*	renamed verbatim/verb to text_raw/txt_raw;	Makarius Wenzel	1999-10-14
\|
*	proof-shell-cd: isar-verbatim no longer required;	Makarius Wenzel	1999-10-07
\|
*	replaced "clear_undo" to "clear_undos";	Makarius Wenzel	1999-10-07
\| \| \| \| \|	replaced "title" by "header"; added "verbatim", "verb";
*	Made new command proof-cd to cd to the directory of the current	David Aspinall	1999-10-06
\| \| \| \| \| \|	buffer. Added a version of it to proof-activate-scripting-hook. Removed cd from initialization sequence. Changed prover specifics accordingly.
*	Fixed proof-showproof-command	David Aspinall	1999-10-06
\|
*	isar-keywords-proof-asm-goal;	Makarius Wenzel	1999-10-01
\|
*	Renamed some configuration variables for uniformity, see CHANGES.	David Aspinall	1999-10-01
\|
*	replaced isar-output-font-lock-terms by isar-output-font-lock-keywords-1;	Makarius Wenzel	1999-09-30
\|
*	proof-find-theorems-command "thms_containing %s;";	Makarius Wenzel	1999-09-30
\| \| \| \| \|	proof-shell-leave-annotations-in-output t; replaced isar-output-font-lock-terms by isar-output-font-lock-keywords-1;
*	added isar-verbatim;	Makarius Wenzel	1999-09-26
\|
*	added thms_containing, ML_setup;	Makarius Wenzel	1999-09-26
\|
*	proof-shell-proof-completed-regexp nil;	Makarius Wenzel	1999-09-25
\|
*	Isabelle term / type hiliting;	Makarius Wenzel	1999-09-24
\|
*	tuned;	Makarius Wenzel	1999-09-24
\|