b : unit -> goalstack

SYNOPSIS

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

DESCRIPTION

The function b is part of the subgoal package. It allows backing up from the last state change (caused by calls to e, g, r, set_goal etc.) The package maintains a backup list of previous proof states. A call to b restores the state to the previous state (which was on top of the backup list).

FAILURE CONDITIONS

The function b will fail if the backup list is empty.

EXAMPLE

  # g `(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])`;;
  val it : goalstack = 1 subgoal (1 total)

  `HD [1; 2; 3] = 1 /\ TL [1; 2; 3] = [2; 3]`

  # e CONJ_TAC;;
  val it : goalstack = 2 subgoals (2 total)

  `TL [1; 2; 3] = [2; 3]`

  `HD [1; 2; 3] = 1`

  # b();;
  val it : goalstack = 1 subgoal (1 total)

  `HD [1; 2; 3] = 1 /\ TL [1; 2; 3] = [2; 3]`

USES

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

SEE ALSO

e, g, p, r, set_goal, top_goal, top_thm.