proof-general/hol-light/TacticRecording, branch master

Remove option aspect of 'finfo' datatype, and rename datatype to 'mldata'.

2012-02-24T12:07:26+00:00

Add wrapper function for :thm -> thm list.
Promote more objects.

Altered graph .dot export so that nodes are displayed as their tactic.

2012-02-23T17:12:05+00:00

* empty log message *

2012-02-23T11:02:46+00:00

Capability for exporting .dot files added.

2012-02-23T11:00:45+00:00

Various small improvements to capability

2012-02-21T14:46:38+00:00

Whole of examples3 now processes
Facility for adding manual labels to atomic/composite tactics

First version of HOL Light tactic recording.

2012-02-16T17:09:21+00:00

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.

proof-general/hol-light/TacticRecording, branch master

Remove option aspect of 'finfo' datatype, and rename datatype to 'mldata'.

Altered graph .dot export so that nodes are displayed as their tactic.

*** empty log message ***

Capability for exporting .dot files added.

Various small improvements to capability

First version of HOL Light tactic recording.

* empty log message *