b : unit -> proof
STRUCTURE
SYNOPSIS
Restores the proof state undoing the effects of a previous expansion.
DESCRIPTION
The function b is part of the subgoal package. It is an abbreviation for the function backup. For a description of the subgoal package, see set_goal.
FAILURE
As for backup.
USES
Back tracking in a goal-directed proof to undo errors or try different tactics.
SEEALSO
HOL  Kananaskis-13