/usr/share/hol88-2.02.19940316/help/ENTRIES/rotate.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 | \DOC rotate
\TYPE {rotate : (int -> void)}
\SYNOPSIS
Reorders the subgoals on top of the subgoal package goal stack.
\DESCRIBE
The function {rotate} is part of the subgoal package. Calling {rotate n} forms
a new proof state. It rotates, by {n} steps, the subgoals in the top level of
the goal stack of the current proof state (i.e., those resulting from the
application of the most recent tactic). Goals are rotated upwards on the stack,
with the top goals being moved to the bottom of the level. If {n} is greater
than the number of goals on the level, the rotation is performed modulo the
number of subgoals. The previous proof state is stored on the backup list, so
may be restored by a call to {backup}. The subgoals of the level are printed
from the bottom of the stack. The function {rotate} is abbreviated by the
function {r}. For a description of the subgoal package, see {set_goal}.
\FAILURE
{rotate} will fail if no goal has been set or if the last goal set has been
completely proved. It will diverge if given a negative argument.
\EXAMPLE
{
#rotate 1;;
evaluation failed rotate_goals
#g "(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3]) /\ (HD (TL[1;2;3]) = 2)";;
"(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3]) /\ (HD(TL[1;2;3]) = 2)"
() : void
#e (REPEAT CONJ_TAC);;
OK..
3 subgoals
"HD(TL[1;2;3]) = 2"
"TL[1;2;3] = [2;3]"
"HD[1;2;3] = 1"
() : void
#rotate 1;;
3 subgoals
"HD[1;2;3] = 1"
"HD(TL[1;2;3]) = 2"
"TL[1;2;3] = [2;3]"
() : void
}
\USES
Proving subgoals in a different order to that generated by the subgoal package.
The subgoals of a goal may be considered in any order. However,
subgoals deeper in the stack cannot be worked on, nor can subgoals higher in
the proof tree.
\SEEALSO
b, backup, backup_limit, e, expand, expandf, g, get_state, p, print_state, r,
save_top_thm, set_goal, set_state, top_goal, top_thm.
\ENDDOC
|