r : int -> unit
Reorders 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.
HOL  Kananaskis-13