proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Update copyright messages and improve the header of elisp files.	Erik Martin-Dorel	2018-02-21
\|
*	Change (eval-when (compile) ...) to (eval-when-compile ...)	Clément Pit--Claudel	2017-05-05
\| \| \| \|	This fixes a bunch of compilation warnings
*	Remove compile-time calls to proof-ready-for-assistant	Clément Pit--Claudel	2017-03-08
\| \| \| \| \|	Compilation used to run in a separate Emacs process for each file, but that's not what happens when installing PG with package.el.
*	Fix incorrect assumption that noninteractive == byte-compiling	Clément Pit--Claudel	2017-03-08
\| \| \| \| \|	The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't.
*	Improvements for type tokens, remove preceding colon	David Aspinall	2015-01-05
\|
*	- support bullets and braces in Prooftree	Hendrik Tews	2013-01-15
\| \| \| \|	- prooftree protocol change to version 3
*	Update	David Aspinall	2012-11-01
\|
*	Remove option aspect of 'finfo' datatype, and rename datatype to 'mldata'.	mark	2012-02-24
\| \| \| \| \|	Add wrapper function for :thm -> thm list. Promote more objects.
*	Altered graph .dot export so that nodes are displayed as their tactic.	mark	2012-02-23
\|
*	Allocate jobs!	David Aspinall	2012-02-23
\|
*	* empty log message *	mark	2012-02-23
\|
*	Capability for exporting .dot files added.	mark	2012-02-23
\|
*	Various small improvements to capability	mark	2012-02-21
\| \| \| \| \|	Whole of examples3 now processes Facility for adding manual labels to atomic/composite tactics
*	* empty log message *	David Aspinall	2012-02-21
\|
*	* empty log message *	David Aspinall	2012-02-21
\|
*	* empty log message *	David Aspinall	2012-02-21
\|
*	First version of HOL Light tactic recording.	mark	2012-02-16
\| \| \| \| \| \| \| \|	See INSTRUCTIONS and LIMITATIONS files for more details. Currently works for flattening "packaged-up" tactic proofs into g/e commands. Won't work for most proofs because most tactics/thms haven't been promoted. Support for exporting proof graph as a series of goal pairs. Support for displaying extra information to be intercepter by PG for Prooftree.
*	Add example menu entry	David Aspinall	2012-02-08
\|
*	Duplicate proof	David Aspinall	2012-02-08
\|
*	Tweak output strings and prompt matching	David Aspinall	2012-02-08
\|
*	Abort attempt to use special exception printing	David Aspinall	2012-02-08
\|
*	Add print_exn for marked up error messages.	David Aspinall	2012-02-08
\|
*	Add restart command (does nothing)	David Aspinall	2012-02-08
\|
*	Add autotest	David Aspinall	2012-02-08
\|
*	Fix pareno	David Aspinall	2012-02-08
\|
*	Add hol-light-prog-name, restart command.	David Aspinall	2012-02-08
\|
*	Try to make evars output match what is expected by Prooftree	David Aspinall	2012-02-08
\|
*	Add proof-forget-id command and make top_thm discard the goalstack.	David Aspinall	2012-02-08
\|
*	Improve handling of undo, implementing pg_kill and pg_undo.	David Aspinall	2012-02-08
\|
*	More progress with Prooftree. Basic trees produced. Undoing needs work.	David Aspinall	2012-02-08
\|
*	Adjust global state idea, it is supposed to count down as well as up...	David Aspinall	2012-02-08
\|
*	Get a little bit further with proof tree.	David Aspinall	2012-02-07
\|
*	Load pg_tactics, fix proof-undo-n-times-cmd again.	David Aspinall	2012-02-07
\|
*	Borrow syntax keywords from caml-mode if available. Typo in undo-n-times.	David Aspinall	2012-02-07
\|
*	Use right HOL system	David Aspinall	2012-02-07
\|
*	Attempt to rebind failwith, which fails, with...errors	David Aspinall	2012-02-07
\|
*	Fix compile	David Aspinall	2012-02-07
\|
*	Pasto	David Aspinall	2012-02-07
\|
*	Start support for both plain and custom top levels (work in progress).	David Aspinall	2012-02-07
\|
*	Draft symbol handling	David Aspinall	2012-01-23
\|
*	Rename goalstate file for pg	David Aspinall	2012-01-20
\|
*	Rename file	David Aspinall	2012-01-20
\|
*	Hint about changing prompt	David Aspinall	2012-01-20
\|
*	Temporary commit to share file, this is work in progress for Prooftree	David Aspinall	2012-01-19
\|
*	Add file from Mark	David Aspinall	2012-01-19
\|
*	Patch needed temporarily to avoid rebuild of Prooftree	David Aspinall	2012-01-19
\|
*	Update documentation	David Aspinall	2012-01-19
\|
*	Improve configuration for HOL Light. Allow goals display to be prefixed by ↵	David Aspinall	2012-01-09
\| \| \| \|	ignored junk (val it : goalstack =).
*	Make configuration settings. Tweak error regexp.	David Aspinall	2012-01-06
\|
*	Some fixes to get a working instance for HOL Light. Work in progress.	David Aspinall	2012-01-05
\|