- 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
set_goal,
restart,
backup,
restore,
save,
set_backup,
expand,
expandf,
p,
top_thm,
top_goal