# HG changeset patch
# User wenzelm
# Date 864117563 -7200
# Node ID 04618aca579de10ab76805516fd6220fa5f48864
# Parent  cee363fc07d796de7755fd12fd72fb6a94693a63
SYNC;

diff -r cee363fc07d7 -r 04618aca579d doc-src/Ref/ref.ind
--- a/doc-src/Ref/ref.ind	Tue May 20 10:28:19 1997 +0200
+++ b/doc-src/Ref/ref.ind	Tue May 20 10:39:23 1997 +0200
@@ -5,7 +5,7 @@
   \item {\tt\$}, \bold{57}, 82
   \item {\tt\%} symbol, 65
   \item *
-    \subitem claset, 127
+    \subitem claset, 128
     \subitem simpset, 106
   \item {\tt ::} symbol, 65, 66
   \item {\tt ==} symbol, 65
@@ -32,23 +32,23 @@
   \item {\tt addaltern}, \bold{124}
   \item {\tt addbefore}, \bold{124}
   \item {\tt addcongs}, 103, \bold{115}, 116
-  \item {\tt AddDs}, \bold{127}
+  \item {\tt AddDs}, \bold{128}
   \item {\tt addDs}, \bold{123}
   \item {\tt addeqcongs}, \bold{103}, 105, 115
-  \item {\tt AddEs}, \bold{127}
+  \item {\tt AddEs}, \bold{128}
   \item {\tt addEs}, \bold{123}
-  \item {\tt AddIs}, \bold{127}
+  \item {\tt AddIs}, \bold{128}
   \item {\tt addIs}, \bold{123}
   \item {\tt addloop}, 104, 105
   \item {\tt addSaltern}, \bold{124}
   \item {\tt addSbefore}, \bold{124}
-  \item {\tt AddSDs}, \bold{127}
+  \item {\tt AddSDs}, \bold{128}
   \item {\tt addSDs}, \bold{123}
-  \item {\tt AddSEs}, \bold{127}
+  \item {\tt AddSEs}, \bold{128}
   \item {\tt addSEs}, \bold{123}
   \item {\tt Addsimps}, \bold{100}, 105, 106
   \item {\tt addsimps}, 102, 105, 106, 116
-  \item {\tt AddSIs}, \bold{127}
+  \item {\tt AddSIs}, \bold{128}
   \item {\tt addSIs}, \bold{123}
   \item {\tt addSolver}, 104, 105
   \item {\tt addss}, \bold{124}, 125
@@ -92,6 +92,7 @@
     \subitem made from parse trees, 80
     \subitem made from terms, 82
   \item {\tt atac}, \bold{19}
+  \item {\tt Auto_tac}, \bold{128}
   \item {\tt axclass} section, 51
   \item axiomatic type class, 51
   \item axioms
@@ -108,7 +109,7 @@
   \item {\tt be}, \bold{11}
   \item {\tt bes}, \bold{11}
   \item {\tt BEST_FIRST}, \bold{31}, 32
-  \item {\tt Best_tac}, \bold{127}
+  \item {\tt Best_tac}, \bold{128}
   \item {\tt best_tac}, \bold{126}
   \item {\tt beta_conversion}, \bold{43}
   \item {\tt bicompose}, \bold{46}
@@ -116,10 +117,10 @@
   \item {\tt bind_thm}, \bold{8}, 9, 37
   \item binders, \bold{74}
   \item {\tt biresolution}, \bold{45}
-  \item {\tt biresolve_tac}, \bold{23}, 128
+  \item {\tt biresolve_tac}, \bold{23}, 129
   \item {\tt Blast.depth_tac}, \bold{125}
   \item {\tt Blast.trace}, \bold{125}
-  \item {\tt Blast_tac}, \bold{127}
+  \item {\tt Blast_tac}, \bold{128}
   \item {\tt blast_tac}, \bold{125}
   \item {\tt Bound}, \bold{57}, 80, 82, 83
   \item {\tt bound_hyp_subst_tac}, \bold{96}
@@ -143,8 +144,8 @@
   \item {\tt claset} ML type, 122
   \item classes
     \subitem context conditions, 52
-  \item classical reasoner, 118--129
-    \subitem setting up, 128
+  \item classical reasoner, 118--130
+    \subitem setting up, 129
     \subitem tactics, 124
   \item classical sets, 122
   \item {\tt ClassicalFun}, 129
@@ -179,8 +180,8 @@
   \indexspace
 
   \item {\tt datatype}, 100
-  \item {\tt Deepen_tac}, \bold{127}
-  \item {\tt deepen_tac}, \bold{126}
+  \item {\tt Deepen_tac}, \bold{128}
+  \item {\tt deepen_tac}, \bold{127}
   \item {\tt defer_tac}, \bold{20}
   \item definitions, \see{rewriting, meta-level}{1}, 20, \bold{51}
     \subitem unfolding, 7, 8
@@ -195,7 +196,7 @@
   \item {\tt DEPTH_FIRST}, \bold{31}
   \item {\tt DEPTH_SOLVE}, \bold{31}
   \item {\tt DEPTH_SOLVE_1}, \bold{31}
-  \item {\tt depth_tac}, \bold{126}
+  \item {\tt depth_tac}, \bold{127}
   \item {\tt Deriv.drop}, \bold{48}
   \item {\tt Deriv.linear}, \bold{48}
   \item {\tt Deriv.size}, \bold{48}
@@ -247,7 +248,7 @@
   \indexspace
 
   \item {\tt fa}, \bold{11}
-  \item {\tt Fast_tac}, \bold{127}
+  \item {\tt Fast_tac}, \bold{128}
   \item {\tt fast_tac}, \bold{126}
   \item {\tt fd}, \bold{11}
   \item {\tt fds}, \bold{11}
@@ -338,7 +339,7 @@
 
   \indexspace
 
-  \item {\tt joinrules}, \bold{128}
+  \item {\tt joinrules}, \bold{129}
 
   \indexspace
 
@@ -374,7 +375,7 @@
   \item meta-implication, 41, 42
   \item meta-quantifiers, 42, 44
   \item meta-rewriting, 7, 12, 13, \bold{20}, 
-		\seealso{tactics, theorems}{130}
+		\seealso{tactics, theorems}{131}
     \subitem in terms, 47
     \subitem in theorems, 38
   \item meta-rules, \see{meta-rules}{1}, 41--47
@@ -550,7 +551,7 @@
   \indexspace
 
   \item {\tt safe_asm_full_simp_tac}, \bold{104}, 105
-  \item {\tt safe_step_tac}, 123, \bold{126}
+  \item {\tt safe_step_tac}, 123, \bold{127}
   \item {\tt safe_tac}, \bold{127}
   \item {\tt save_proof}, \bold{14}
   \item saving your work, \bold{1}
@@ -559,7 +560,7 @@
   \item {\tt SELECT_GOAL}, 20, \bold{33}
   \item {\tt Sequence.seq} ML type, 25
   \item sequences (lazy lists), \bold{26}
-  \item sequent calculus, 118
+  \item sequent calculus, 119
   \item sessions, 1--5
   \item {\tt set}, 3
   \item {\tt set_current_thy}, 101
@@ -617,7 +618,7 @@
   \item {\tt standard}, \bold{39}
   \item starting up, \bold{1}
   \item {\tt STATE}, \bold{25}
-  \item {\tt Step_tac}, \bold{127}
+  \item {\tt Step_tac}, \bold{128}
   \item {\tt step_tac}, 123, \bold{127}
   \item {\tt store_thm}, \bold{8}
   \item {\tt string_of_cterm}, \bold{59}
@@ -634,7 +635,7 @@
     \subitem rules, 95
   \item {\tt swap} theorem, \bold{129}
   \item {\tt swap_res_tac}, \bold{128}
-  \item {\tt swapify}, \bold{128}
+  \item {\tt swapify}, \bold{129}
   \item {\tt sym} theorem, 96, \bold{97}
   \item {\tt symmetric}, \bold{43}
   \item {\tt syn_of}, \bold{68}