# HG changeset patch
# User paulson
# Date 886858695 -3600
# Node ID cdf16a9fb2ce114d3fa0d86c30a92d7c9e0e134b
# Parent  6759ba6d3cc1d4031eaadd38c1d970ff90a8c7ca
auto update

diff -r 6759ba6d3cc1 -r cdf16a9fb2ce doc-src/Ref/ref.ind
--- a/doc-src/Ref/ref.ind	Sat Feb 07 14:37:48 1998 +0100
+++ b/doc-src/Ref/ref.ind	Sat Feb 07 14:38:15 1998 +0100
@@ -77,7 +77,7 @@
   \item {\tt asm_simp_tac}, \bold{112}, 125
   \item {\tt asm_simplify}, 113
   \item associative-commutative operators, 118
-  \item {\tt assume}, \bold{43}
+  \item {\tt assume}, \bold{44}
   \item {\tt assume_ax}, 9, \bold{57}
   \item {\tt assume_tac}, \bold{18}, 131
   \item {\tt assumption}, \bold{47}
@@ -116,7 +116,7 @@
   \item {\tt Best_tac}, \bold{137}
   \item {\tt best_tac}, \bold{136}
   \item {\tt beta_conversion}, \bold{45}
-  \item {\tt bicompose}, \bold{47}
+  \item {\tt bicompose}, \bold{48}
   \item {\tt bimatch_tac}, \bold{24}
   \item {\tt bind_thm}, \bold{9}, 10, 38
   \item binders, \bold{78}
@@ -164,7 +164,7 @@
   \item {\tt compose_tac}, \bold{24}
   \item {\tt compSWrapper}, \bold{133}
   \item {\tt compWrapper}, \bold{133}
-  \item {\tt concl_of}, \bold{40}
+  \item {\tt concl_of}, \bold{41}
   \item {\tt COND}, \bold{33}
   \item congruence rules, 109
   \item {\tt Const}, \bold{60}, 86, 96
@@ -175,7 +175,7 @@
   \item {\tt context}, 103
   \item {\tt contr_tac}, \bold{138}
   \item {\tt could_unify}, \bold{26}
-  \item {\tt cprems_of}, \bold{40}
+  \item {\tt cprems_of}, \bold{41}
   \item {\tt cprop_of}, \bold{40}
   \item {\tt CPure} theory, 51
   \item {\tt CPure.thy}, \bold{58}
@@ -251,6 +251,7 @@
   \item equality, 99--102
   \item {\tt eres_inst_tac}, \bold{19}
   \item {\tt eresolve_tac}, \bold{17}
+    \subitem on other than first premise, 40
   \item {\tt ERROR}, 5
   \item {\tt error}, 5
   \item error messages, 5
@@ -304,8 +305,8 @@
   \item {\tt forall_elim_var}, \bold{46}
   \item {\tt forall_elim_vars}, \bold{46}
   \item {\tt forall_intr}, \bold{45}
-  \item {\tt forall_intr_frees}, \bold{45}
-  \item {\tt forall_intr_list}, \bold{45}
+  \item {\tt forall_intr_frees}, \bold{46}
+  \item {\tt forall_intr_list}, \bold{46}
   \item {\tt force_strip_shyps}, \bold{41}
   \item {\tt forw_inst_tac}, \bold{19}
   \item forward proof, 18, 38
@@ -364,7 +365,7 @@
   \item {\tt instance} section, 53
   \item {\tt instantiate}, \bold{46}
   \item {\tt instantiate'}, \bold{39}, 46
-  \item instantiation, 18, 39, 46
+  \item instantiation, 19, 39, 46
   \item {\tt INTLEAVE}, \bold{29}, 31
   \item {\tt INTLEAVE'}, 36
   \item {\tt invoke_oracle}, \bold{64}
@@ -403,9 +404,9 @@
   \item {\tt max_pri}, 68, \bold{74}
   \item {\tt merge_ss}, \bold{106}
   \item {\tt merge_theories}, \bold{58}
-  \item meta-assumptions, 34, 42, 43, 47
+  \item meta-assumptions, 34, 42, 44, 47
     \subitem printing of, 4
-  \item meta-equality, 43, 44
+  \item meta-equality, 43--45
   \item meta-implication, 43, 44
   \item meta-quantifiers, 43, 45
   \item meta-rewriting, 8, 13, 14, \bold{21}, 
@@ -461,7 +462,7 @@
   \item {\tt pop_proof}, \bold{15}
   \item {\tt pr}, \bold{11}
   \item {\tt premises}, \bold{8}, 15
-  \item {\tt prems_of}, \bold{40}
+  \item {\tt prems_of}, \bold{41}
   \item {\tt prems_of_ss}, \bold{110}
   \item pretty printing, 74, 76--77, 93
   \item {\tt Pretty.setdepth}, \bold{4}
@@ -541,7 +542,7 @@
   \item reading
     \subitem axioms, \see{{\tt assume_ax}}{51}
     \subitem goals, \see{proofs, starting}{7}
-  \item {\tt reflexive}, \bold{44}
+  \item {\tt reflexive}, \bold{45}
   \item {\tt ren}, \bold{13}
   \item {\tt rename_last_tac}, \bold{22}
   \item {\tt rename_params_rule}, \bold{48}
@@ -577,6 +578,7 @@
   \item {\tt rewtac}, \bold{20}
   \item {\tt RL}, \bold{38}
   \item {\tt RLN}, \bold{38}
+  \item {\tt rotate_prems}, \bold{40}
   \item {\tt rotate_proof}, \bold{15}
   \item {\tt rotate_tac}, \bold{23}
   \item {\tt RS}, \bold{38}
@@ -612,7 +614,7 @@
   \item {\tt settermless}, \bold{117}
   \item {\tt setWrapper}, \bold{133}
   \item shortcuts
-    \subitem for tactics, 19
+    \subitem for tactics, 20
     \subitem for {\tt by} commands, 11
   \item {\tt show_brackets}, \bold{4}
   \item {\tt show_consts}, \bold{4}
@@ -675,7 +677,7 @@
   \item subgoal module, 7--16
   \item {\tt subgoal_tac}, \bold{20}
   \item {\tt subgoals_of_brl}, \bold{24}
-  \item {\tt subgoals_tac}, \bold{20}
+  \item {\tt subgoals_tac}, \bold{21}
   \item {\tt subst} theorem, 99, \bold{102}
   \item substitution
     \subitem rules, 99
@@ -684,7 +686,7 @@
   \item {\tt swap_res_tac}, \bold{138}
   \item {\tt swapify}, \bold{138}
   \item {\tt sym} theorem, 100, \bold{102}
-  \item {\tt symmetric}, \bold{44}
+  \item {\tt symmetric}, \bold{45}
   \item {\tt syn_of}, \bold{72}
   \item syntax
     \subitem Pure, 68--73
@@ -717,7 +719,7 @@
     \subitem scanning for subgoals, 35
     \subitem searching, 32
   \item tactics, 17--28
-    \subitem assumption, \bold{18}, 19
+    \subitem assumption, \bold{18}, 20
     \subitem commands for applying, 8
     \subitem debugging, 15
     \subitem filtering results of, 31
@@ -725,11 +727,11 @@
     \subitem for contradiction, 138
     \subitem for inserting facts, 20
     \subitem for Modus Ponens, 138
-    \subitem instantiation, 18
+    \subitem instantiation, 19
     \subitem matching, 18
-    \subitem meta-rewriting, 19, \bold{21}
+    \subitem meta-rewriting, 20, \bold{21}
     \subitem primitives for coding, 26
-    \subitem resolution, \bold{17}, 19, 24, 25
+    \subitem resolution, \bold{17}, 20, 24, 25
     \subitem restricting to a subgoal, 34
     \subitem simplification, 112
     \subitem substitution, 99--102