forget_historyproofManagerLib.forget_history : unit -> unitClears the proof history.
The function forget_history is part of the subgoal
package. A call to forget_history clears the history of
saved proof states. Subsequent calls to backup or
restart will behave as if the initial goal was the state at
the time of the call to forget_history. For a description
of the subgoal package, see set_goal.
The function forget_history only fails if no goalstack
is being managed.
Hiding an automatic preprocessing phase of a proof before handing it to the user.
proofManagerLib.set_goal,
proofManagerLib.restart,
proofManagerLib.backup,
proofManagerLib.redo,
proofManagerLib.restore,
proofManagerLib.save,
proofManagerLib.set_backup,
proofManagerLib.expand,
proofManagerLib.expandf,
proofManagerLib.p, proofManagerLib.top_thm,
proofManagerLib.top_goal