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.
FAILURE
The function forget_history only fails if no goalstack is being managed.
USES
Hiding an automatic preprocessing phase of a proof before handing it to the user.