forget_history : unit -> unit
STRUCTURE
SYNOPSIS
Clears the proof history.
DESCRIPTION
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.
SEEALSO
HOL  Trindemossen-1