r : int -> unit
STRUCTURE
proofManagerLib
SYNOPSIS
Reorders the subgoals on top of the subgoal package goal stack.
DESCRIPTION
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.

FAILURE
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.
USES
Interactively attacking subgoals in a different order to that generated by the subgoal package.
SEEALSO
set_goal, restart, backup, restore, save, set_backup, expand, expandf, p, top_thm, top_goal
HOL  Trindemossen-1