#
c7b36e85 |
|
15-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Up to hol.state0
|
#
fce4b42a |
|
20-Dec-2014 |
Jeremy Dawson <jeremy@cecs.anu.edu.au> |
added flatn command in proofManagerLib in interactive proof, to flatten subgoal stack, so as to merge current list of subgoals with previous level(s)
|
#
876ff199 |
|
11-Dec-2014 |
Jeremy Dawson <jeremy@cecs.anu.edu.au> |
expand_list to interactively work on a list of subgoals also Tactical.VALID_LT, to check that a list-tactical is valid (expand_list checks validity, expand_listf doesn't) also abbreviations elt, eall, eta, enth to apply (list-)tactic to subgoal(s)
|
#
e2cfde40 |
|
11-Feb-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
renaming of functions Backup -> restore save_proof -> save Having two functions "Backup" and "backup" around caused trouble with documentation.
|
#
0116760b |
|
04-Feb-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
I added another layer of backups / undos to proofManagerLib. The existing backup-facility records all applications of tactis (by default the last 15 steps) and the function proofManagerLib.backup allows undoing the last step. This is very useful. However, it is sometimes useful to be able to got back to user-defined save-points instead of just auto-recorded last steps. Therefore, I added two new functions to proofManagerLib (with corresponding ones in Manager and History): val Backup : unit -> proof val save_proof : unit -> proof save_proof allows to store the current status of the proof. All the existing auto-undo history is deleted. So you can't easily go back before that point any more. You can then continue your proof and use the normal undo as well. At some point, you might want to undo everything up to this save-point. That's done by Backup. If no save-point has been set, Backup returns to the initial goal, i.e. it behaves like restart. In constrast to backup, Backup does not delete the save-point by default. So you can go back, re-try the proof from there, and go back again. If you are already at a save-point (backup fails), then Backup will delete the current save-point and go back to the previous one.
|
#
7f50036f |
|
24-Jan-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
New function "forget_history" added to proofManagerLib. This function can be used during interactive proofs to forbit undos past the current point. Even restarting the proof will return you to the status, when forget_history was executed.
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
7b11d4a6 |
|
14-Jun-2008 |
Konrad Slind <konrad.slind@gmail.com> |
Added proofManagerLib. This adds a type of "goal trees" as an alternative to goalstacks. Relevant entrypoints: gt ` .... ` -- start a goaltree proof, analogous to g eq ` ... ` -- expand a tactic, analogous to e (except that the text of the tactic is delimited by quotes). A goaltree manages the construction of the final tactic, so should ease some of the script maintenance that the goalstack requires. Backup and restart are just as for goalstacks. All the entrypoints for goalstacks are just as they were before; there shouldn't be any difference.
|