b

proofManagerLib.b : unit -> proof

Restores the proof state undoing the effects of a previous expansion.

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.

Back tracking in a goal-directed proof to undo errors or try different tactics.

See also

proofManagerLib.set_goal, proofManagerLib.restart, proofManagerLib.backup, proofManagerLib.rd, proofManagerLib.redo, proofManagerLib.restore, proofManagerLib.save, proofManagerLib.set_backup, proofManagerLib.expand, proofManagerLib.expandf, proofManagerLib.p, proofManagerLib.top_thm, proofManagerLib.top_goal