proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	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
\|
*	* 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
*	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.