| Age | Commit message (Collapse) | Author |
|---|
|
Add wrapper function for :thm -> thm list.
Promote more objects.
|
|
Whole of examples3 now processes
Facility for adding manual labels to atomic/composite tactics
|
|
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.
|
