# HG changeset patch
# User paulson
# Date 875698255 -7200
# Node ID 5617a56983453da143e9031cfcdce7cab7e57b81
# Parent  f3d35f501ec1ac536592ac6e029e1c5b9c577b2d
Auto update

diff -r f3d35f501ec1 -r 5617a5698345 doc-src/Ref/ref.ind
--- a/doc-src/Ref/ref.ind	Tue Sep 30 17:33:16 1997 +0200
+++ b/doc-src/Ref/ref.ind	Wed Oct 01 11:30:55 1997 +0200
@@ -78,7 +78,7 @@
   \item {\tt assume_tac}, \bold{17}, 122
   \item {\tt assumption}, \bold{45}
   \item assumptions
-    \subitem contradictory, 128
+    \subitem contradictory, 129
     \subitem deleting, 22
     \subitem in simplification, 99, 104
     \subitem inserting, 19
@@ -110,7 +110,7 @@
   \item {\tt bes}, \bold{11}
   \item {\tt BEST_FIRST}, \bold{31}, 32
   \item {\tt Best_tac}, \bold{128}
-  \item {\tt best_tac}, \bold{126}
+  \item {\tt best_tac}, \bold{127}
   \item {\tt beta_conversion}, \bold{43}
   \item {\tt bicompose}, \bold{46}
   \item {\tt bimatch_tac}, \bold{23}
@@ -118,10 +118,10 @@
   \item binders, \bold{74}
   \item {\tt biresolution}, \bold{45}
   \item {\tt biresolve_tac}, \bold{23}, 129
-  \item {\tt Blast.depth_tac}, \bold{125}
-  \item {\tt Blast.trace}, \bold{125}
+  \item {\tt Blast.depth_tac}, \bold{126}
+  \item {\tt Blast.trace}, \bold{126}
   \item {\tt Blast_tac}, \bold{128}
-  \item {\tt blast_tac}, \bold{125}
+  \item {\tt blast_tac}, \bold{126}
   \item {\tt Bound}, \bold{57}, 80, 82, 83
   \item {\tt bound_hyp_subst_tac}, \bold{96}
   \item {\tt br}, \bold{11}
@@ -139,16 +139,20 @@
   \item {\tt CHANGED}, \bold{30}
   \item {\tt chop}, \bold{9}, 13
   \item {\tt choplev}, \bold{9}
+  \item {\tt Clarify_step_tac}, \bold{128}
+  \item {\tt clarify_step_tac}, \bold{125}
+  \item {\tt Clarify_tac}, \bold{128}
+  \item {\tt clarify_tac}, \bold{125}
   \item claset
-    \subitem current, 127
+    \subitem current, 128
   \item {\tt claset} ML type, 122
   \item classes
     \subitem context conditions, 52
   \item classical reasoner, 118--130
     \subitem setting up, 129
-    \subitem tactics, 124
+    \subitem tactics, 125
   \item classical sets, 122
-  \item {\tt ClassicalFun}, 129
+  \item {\tt ClassicalFun}, 130
   \item {\tt combination}, \bold{44}
   \item {\tt commit}, \bold{2}
   \item {\tt COMP}, \bold{46}
@@ -164,7 +168,7 @@
   \item constants, \bold{57}
     \subitem for translations, 69
     \subitem syntactic, 84
-  \item {\tt contr_tac}, \bold{128}
+  \item {\tt contr_tac}, \bold{129}
   \item {\tt could_unify}, \bold{24}
   \item {\tt CPure} theory, 49
   \item {\tt CPure.thy}, \bold{55}
@@ -224,7 +228,7 @@
   \item {\tt empty_ss}, 105, 116
   \item {\tt eq_assume_tac}, \bold{17}, 122
   \item {\tt eq_assumption}, \bold{45}
-  \item {\tt eq_mp_tac}, \bold{128}
+  \item {\tt eq_mp_tac}, \bold{129}
   \item {\tt eq_reflection} theorem, \bold{97}, 113
   \item {\tt eq_thm}, \bold{32}
   \item {\tt equal_elim}, \bold{43}
@@ -252,7 +256,7 @@
 
   \item {\tt fa}, \bold{11}
   \item {\tt Fast_tac}, \bold{128}
-  \item {\tt fast_tac}, \bold{126}
+  \item {\tt fast_tac}, \bold{127}
   \item {\tt fd}, \bold{11}
   \item {\tt fds}, \bold{11}
   \item {\tt fe}, \bold{11}
@@ -310,8 +314,8 @@
 
   \item {\tt has_fewer_prems}, \bold{32}
   \item {\tt hyp_subst_tac}, \bold{96}
-  \item {\tt hyp_subst_tacs}, \bold{129}
-  \item {\tt HypsubstFun}, 97, 129
+  \item {\tt hyp_subst_tacs}, \bold{130}
+  \item {\tt HypsubstFun}, 97, 130
 
   \indexspace
 
@@ -331,7 +335,7 @@
   \item {\tt indexname} ML type, 57, 67
   \item infixes, \bold{73}
   \item {\tt insert} constant, 88
-  \item {\tt inst_step_tac}, \bold{127}
+  \item {\tt inst_step_tac}, \bold{128}
   \item {\tt instance} section, 51
   \item {\tt instantiate}, \bold{45}
   \item instantiation, 17, 38, 45
@@ -386,8 +390,8 @@
   \item {\tt mk_case_split_tac}, \bold{116}
   \item {\tt ML} section, 51, 91, 93
   \item model checkers, 75
-  \item {\tt mp} theorem, \bold{129}
-  \item {\tt mp_tac}, \bold{128}
+  \item {\tt mp} theorem, \bold{130}
+  \item {\tt mp_tac}, \bold{129}
   \item {\tt MRL}, \bold{37}
   \item {\tt MRS}, \bold{37}
 
@@ -400,7 +404,7 @@
   \item {\tt net_resolve_tac}, \bold{24}
   \item {\tt no_tac}, \bold{30}
   \item {\tt None}, \bold{26}
-  \item {\tt not_elim} theorem, \bold{129}
+  \item {\tt not_elim} theorem, \bold{130}
   \item {\tt nprems_of}, \bold{39}
   \item numerals, 66
 
@@ -481,6 +485,8 @@
   \item {\tt prthq}, \bold{37}
   \item {\tt prths}, \bold{37}
   \item {\tt prune_params_tac}, \bold{22}
+  \item {\tt pttrn} nonterminal, \bold{66}
+  \item {\tt pttrns} nonterminal, \bold{66}
   \item {\tt Pure} theory, 49, 64, 68
   \item {\tt Pure.thy}, \bold{55}
   \item {\tt push_proof}, \bold{14}
@@ -553,7 +559,9 @@
   \indexspace
 
   \item {\tt safe_asm_full_simp_tac}, \bold{104}, 105
+  \item {\tt Safe_step_tac}, \bold{128}
   \item {\tt safe_step_tac}, 123, \bold{127}
+  \item {\tt Safe_tac}, \bold{128}
   \item {\tt safe_tac}, \bold{127}
   \item {\tt save_proof}, \bold{14}
   \item saving your work, \bold{1}
@@ -599,11 +607,11 @@
   \item {\tt simpset} ML type, 105
   \item {\tt simpset} ML value, 101
   \item {\tt simpset_of}, 106
-  \item {\tt size_of_thm}, 31, \bold{32}, 129
-  \item {\tt sizef}, \bold{129}
-  \item {\tt slow_best_tac}, \bold{126}
-  \item {\tt slow_step_tac}, 123, \bold{127}
-  \item {\tt slow_tac}, \bold{126}
+  \item {\tt size_of_thm}, 31, \bold{32}, 130
+  \item {\tt sizef}, \bold{130}
+  \item {\tt slow_best_tac}, \bold{127}
+  \item {\tt slow_step_tac}, 124, \bold{128}
+  \item {\tt slow_tac}, \bold{127}
   \item {\tt Some}, \bold{26}
   \item {\tt SOMEGOAL}, \bold{34}
   \item {\tt sort} nonterminal, \bold{66}
@@ -620,7 +628,7 @@
   \item {\tt standard}, \bold{39}
   \item starting up, \bold{1}
   \item {\tt Step_tac}, \bold{128}
-  \item {\tt step_tac}, 123, \bold{127}
+  \item {\tt step_tac}, 124, \bold{128}
   \item {\tt store_thm}, \bold{8}
   \item {\tt string_of_cterm}, \bold{59}
   \item {\tt string_of_ctyp}, \bold{60}
@@ -634,8 +642,8 @@
   \item {\tt subst} theorem, 95, \bold{97}
   \item substitution
     \subitem rules, 95
-  \item {\tt swap} theorem, \bold{129}
-  \item {\tt swap_res_tac}, \bold{128}
+  \item {\tt swap} theorem, \bold{130}
+  \item {\tt swap_res_tac}, \bold{129}
   \item {\tt swapify}, \bold{129}
   \item {\tt sym} theorem, 96, \bold{97}
   \item {\tt symmetric}, \bold{43}
@@ -676,9 +684,9 @@
     \subitem debugging, 14
     \subitem filtering results of, 30
     \subitem for composition, 22
-    \subitem for contradiction, 128
+    \subitem for contradiction, 129
     \subitem for inserting facts, 19
-    \subitem for Modus Ponens, 128
+    \subitem for Modus Ponens, 129
     \subitem instantiation, 17
     \subitem matching, 17
     \subitem meta-rewriting, 18, \bold{20}
@@ -746,7 +754,7 @@
   \item {\tt trace_REPEAT}, \bold{29}
   \item {\tt trace_simp}, 100, 107
   \item tracing
-    \subitem of classical prover, 125
+    \subitem of classical prover, 126
     \subitem of macros, 88
     \subitem of searching tacticals, 31
     \subitem of simplification, 100, 107--108