The function restart is part of the subgoal package. A call to restart
clears the proof history and returns to the initial goal. After a call to
restart, the proof state is the same as it was after the inital call to
set_goal (or g). For a description of the subgoal package, see set_goal.