rotate : int -> refinement

SYNOPSIS: Rotate a goalstate.
DESCRIPTION: The function rotate n gl rotates a list gl of subgoals by n places. The function r is the special case where this modification is applied to the imperative variable of unproven subgoals.
FAILURE CONDITIONS: Fails only if the list of goals is empty.
SEE ALSO: r.