rproofManagerLib.r : int -> unitReorders the subgoals on top of the subgoal package goal stack.
The function r is part of the subgoal package. The name
rotate may also be used to access the same function. For a
general description of the subgoal package, see
set_goal.
The r function’s basic step of operation is to take the
first element of the current list of sub-goals and move it to the end of
the same list. The numeric argument passed to r specifies
how many times this operation is to be performed.
Raises the NO_PROOFS exception if there is no current
proof manipulated by the subgoal package. Raises a HOL_ERR
if the current goal state only has one sub-goal, or if the argument
passed to r is negative.
Interactively attacking subgoals in a different order to that generated by the subgoal package.
proofManagerLib.set_goal,
proofManagerLib.restart,
proofManagerLib.backup,
proofManagerLib.redo,
proofManagerLib.restore,
proofManagerLib.save,
proofManagerLib.set_backup,
proofManagerLib.expand,
proofManagerLib.expandf,
proofManagerLib.p, proofManagerLib.top_thm,
proofManagerLib.top_goal