aboutsummaryrefslogtreecommitdiff
path: root/hol-light/pg_tactics.ml
AgeCommit message (Collapse)Author
2012-02-08Tweak output strings and prompt matchingDavid Aspinall
2012-02-08Add restart command (does nothing)David Aspinall
2012-02-08Try to make evars output match what is expected by ProoftreeDavid Aspinall
2012-02-08Add proof-forget-id command and make top_thm discard the goalstack.David Aspinall
2012-02-08Improve handling of undo, implementing pg_kill and pg_undo.David Aspinall
2012-02-08Adjust global state idea, it is supposed to count down as well as up...David Aspinall
2012-02-07Start support for both plain and custom top levels (work in progress).David Aspinall
2012-01-20Rename fileDavid Aspinall