# HG changeset patch
# User paulson
# Date 862410823 -7200
# Node ID d4bed82315abc533ed397ec3d6eb5badbd1999bd
# Parent  a2de0be6e14d52b83bfc30187a357d64e97b9513
Indexing for trace_simp

diff -r a2de0be6e14d -r d4bed82315ab doc-src/Ref/ref.ind
--- a/doc-src/Ref/ref.ind	Wed Apr 30 13:40:40 1997 +0200
+++ b/doc-src/Ref/ref.ind	Wed Apr 30 16:33:43 1997 +0200
@@ -1,296 +1,300 @@
 \begin{theindex}
 
-  \item {\ptt !!} symbol, 69
+  \item {\ptt !!} symbol, 64
     \subitem in main goal, 7
-  \item {\tt\$}, \bold{61}, 86
-  \item {\tt\%} symbol, 69
+  \item {\tt\$}, \bold{56}, 79
+  \item {\tt\%} symbol, 64
   \item *
-    \subitem claset, 129
-    \subitem simpset, 109
-  \item {\ptt ::} symbol, 69, 70
-  \item {\ptt ==} symbol, 69
-  \item {\ptt ==>} symbol, 69
-  \item {\ptt =>} symbol, 69
-  \item {\ptt =?=} symbol, 69
-  \item {\tt\at Enum} constant, 92
-  \item {\tt\at Finset} constant, 92, 93
-  \item {\ptt [} symbol, 69
-  \item {\ptt [|} symbol, 69
-  \item {\ptt ]} symbol, 69
-  \item {\ptt _K} constant, 94, 96
-  \item \verb'{}' symbol, 92
-  \item {\tt\ttlbrace} symbol, 69
-  \item {\tt\ttrbrace} symbol, 69
-  \item {\ptt |]} symbol, 69
+    \subitem claset, 121
+    \subitem simpset, 99
+  \item {\ptt ::} symbol, 64, 65
+  \item {\ptt ==} symbol, 64
+  \item {\ptt ==>} symbol, 64
+  \item {\ptt =>} symbol, 64
+  \item {\ptt =?=} symbol, 64
+  \item {\tt\at Enum} constant, 85
+  \item {\tt\at Finset} constant, 85
+  \item {\ptt [} symbol, 64
+  \item {\ptt [|} symbol, 64
+  \item {\ptt ]} symbol, 64
+  \item {\ptt _K} constant, 86, 88
+  \item \verb'{}' symbol, 85
+  \item {\tt\ttlbrace} symbol, 64
+  \item {\tt\ttrbrace} symbol, 64
+  \item {\ptt |]} symbol, 64
 
   \indexspace
 
-  \item {\ptt Abs}, \bold{61}, 86
-  \item {\ptt abstract_over}, \bold{62}
-  \item {\ptt abstract_rule}, \bold{45}
-  \item {\ptt aconv}, \bold{62}
-  \item {\ptt addaltern}, \bold{127}
-  \item {\ptt addbefore}, \bold{127}
-  \item {\ptt addcongs}, 106, \bold{118}, 119
-  \item {\ptt AddDs}, \bold{129}
-  \item {\ptt addDs}, \bold{126}
-  \item {\ptt addeqcongs}, \bold{106}, 108, 118
-  \item {\ptt AddEs}, \bold{129}
-  \item {\ptt addEs}, \bold{126}
-  \item {\ptt AddIs}, \bold{129}
-  \item {\ptt addIs}, \bold{126}
-  \item {\ptt addloop}, 107, 108
-  \item {\ptt addSaltern}, \bold{127}
-  \item {\ptt addSbefore}, \bold{127}
-  \item {\ptt AddSDs}, \bold{129}
-  \item {\ptt addSDs}, \bold{126}
-  \item {\ptt AddSEs}, \bold{129}
-  \item {\ptt addSEs}, \bold{125}
-  \item {\ptt Addsimps}, \bold{103}, 108, 109
-  \item {\ptt addsimps}, 105, 108, 109, 119
-  \item {\ptt AddSIs}, \bold{129}
-  \item {\ptt addSIs}, \bold{125}
-  \item {\ptt addSolver}, 107, 108
-  \item {\ptt addss}, 126, \bold{127}
-  \item {\ptt addSSolver}, 107, 108
-  \item {\ptt all_tac}, \bold{30}
-  \item {\ptt ALLGOALS}, \bold{34}, 111, 115
+  \item {\ptt Abs}, \bold{56}, 79
+  \item {\ptt abstract_over}, \bold{57}
+  \item {\ptt abstract_rule}, \bold{41}
+  \item {\ptt aconv}, \bold{57}
+  \item {\ptt addaltern}, \bold{118}
+  \item {\ptt addbefore}, \bold{118}
+  \item {\ptt addcongs}, 97, 110, \bold{110}
+  \item {\ptt AddDs}, \bold{121}
+  \item {\ptt addDs}, \bold{116}
+  \item {\ptt addeqcongs}, \bold{97}, 100, 110
+  \item {\ptt AddEs}, \bold{121}
+  \item {\ptt addEs}, \bold{116}
+  \item {\ptt AddIs}, \bold{121}
+  \item {\ptt addIs}, \bold{116}
+  \item {\ptt addloop}, 99, 100
+  \item {\ptt addSaltern}, \bold{118}
+  \item {\ptt addSbefore}, \bold{118}
+  \item {\ptt AddSDs}, \bold{121}
+  \item {\ptt addSDs}, \bold{116}
+  \item {\ptt AddSEs}, \bold{121}
+  \item {\ptt addSEs}, \bold{116}
+  \item {\ptt Addsimps}, \bold{95}, 99, 100
+  \item {\ptt addsimps}, 96, 99, 100, 110
+  \item {\ptt AddSIs}, \bold{121}
+  \item {\ptt addSIs}, \bold{116}
+  \item {\ptt addSolver}, 98, 100
+  \item {\ptt addss}, 117, \bold{117}, 118
+  \item {\ptt addSSolver}, 98, 100
+  \item {\ptt all_tac}, \bold{27}
+  \item {\ptt ALLGOALS}, \bold{32}, 103, 106
   \item ambiguity
-    \subitem of parsed expressions, 78
-  \item {\ptt any} nonterminal, \bold{68}
-  \item {\ptt APPEND}, \bold{28}, 30
-  \item {\ptt APPEND'}, 35
-  \item {\ptt Appl}, 83
-  \item {\ptt aprop} nonterminal, \bold{70}
-  \item {\ptt ares_tac}, \bold{19}
-  \item {\ptt args} nonterminal, 93
-  \item {\ptt Arith} theory, 114
+    \subitem of parsed expressions, 72
+  \item {\ptt any} nonterminal, \bold{63}
+  \item {\ptt APPEND}, \bold{26}, 27
+  \item {\ptt APPEND'}, 33
+  \item {\ptt Appl}, 76
+  \item {\ptt aprop} nonterminal, \bold{63}
+  \item {\ptt ares_tac}, \bold{18}
+  \item {\ptt args} nonterminal, 85
+  \item {\ptt Arith} theory, 105
   \item arities
-    \subitem context conditions, 52
-  \item {\ptt Asm_full_simp_tac}, \bold{103}, 108
-  \item {\ptt asm_full_simp_tac}, 22, 108, \bold{109}, 112
-  \item {\ptt asm_rl} theorem, 21
-  \item {\ptt Asm_simp_tac}, \bold{103}, 108
-  \item {\ptt asm_simp_tac}, 108, \bold{109}, 110, 119
-  \item associative-commutative operators, 113
-  \item {\ptt assume}, \bold{43}
-  \item {\ptt assume_ax}, 8, \bold{56}
-  \item {\ptt assume_tac}, \bold{17}, 125
-  \item {\ptt assumption}, \bold{46}
+    \subitem context conditions, 48
+  \item {\ptt Asm_full_simp_tac}, \bold{95}, 100
+  \item {\ptt asm_full_simp_tac}, 20, \bold{99}, 100, 104
+  \item {\ptt asm_rl} theorem, 19
+  \item {\ptt Asm_simp_tac}, \bold{94}, 100
+  \item {\ptt asm_simp_tac}, \bold{99}, 100, 102, 110
+  \item associative-commutative operators, 105
+  \item {\ptt assume}, \bold{40}
+  \item {\ptt assume_ax}, 8, \bold{52}
+  \item {\ptt assume_tac}, \bold{16}, 116
+  \item {\ptt assumption}, \bold{43}
   \item assumptions
-    \subitem contradictory, 129
-    \subitem deleting, 22
-    \subitem in simplification, 102, 107
-    \subitem inserting, 19
-    \subitem negated, 123
-    \subitem of main goal, 7--9, 14
-    \subitem reordering, 112
-    \subitem rotating, 22
-    \subitem substitution in, 99
-    \subitem tactics for, 17
-  \item ASTs, 83--88
-    \subitem made from parse trees, 84
-    \subitem made from terms, 86
-  \item {\ptt atac}, \bold{19}
+    \subitem contradictory, 121
+    \subitem deleting, 20
+    \subitem in simplification, 94, 98
+    \subitem inserting, 18
+    \subitem negated, 114
+    \subitem of main goal, 6, 8, 13
+    \subitem reordering, 104
+    \subitem rotating, 20
+    \subitem substitution in, 91
+    \subitem tactics for, 16
+  \item ASTs, 76--80
+    \subitem made from parse trees, 77
+    \subitem made from terms, 79
+  \item {\ptt atac}, \bold{17}
   \item axioms
-    \subitem extracting, 56
-  \item {\ptt axioms_of}, \bold{57}
+    \subitem extracting, 51
+  \item {\ptt axioms_of}, \bold{52}
 
   \indexspace
 
-  \item {\ptt ba}, \bold{11}
+  \item {\ptt ba}, \bold{10}
   \item {\ptt back}, \bold{9}
-  \item batch execution, 12
-  \item {\ptt bd}, \bold{11}
-  \item {\ptt bds}, \bold{11}
-  \item {\ptt be}, \bold{11}
-  \item {\ptt bes}, \bold{11}
-  \item {\ptt BEST_FIRST}, \bold{31}, 32
-  \item {\ptt Best_tac}, \bold{129}
-  \item {\ptt best_tac}, \bold{127}
-  \item {\ptt beta_conversion}, \bold{44}
-  \item {\ptt bicompose}, \bold{47}
-  \item {\ptt bimatch_tac}, \bold{23}
-  \item {\ptt bind_thm}, \bold{8}, 9, 38
-  \item binders, \bold{77}
-  \item {\ptt biresolution}, \bold{46}
-  \item {\ptt biresolve_tac}, \bold{23}, 130
-  \item {\ptt Bound}, \bold{61}, 84, 86, 87
-  \item {\ptt bound_hyp_subst_tac}, \bold{99}
-  \item {\ptt br}, \bold{11}
-  \item {\ptt BREADTH_FIRST}, \bold{31}
-  \item {\ptt brs}, \bold{11}
-  \item {\ptt bw}, \bold{12}
-  \item {\ptt bws}, \bold{12}
-  \item {\ptt by}, \bold{7}, 9, 10, 15
+  \item batch execution, 11
+  \item {\ptt bd}, \bold{10}
+  \item {\ptt bds}, \bold{10}
+  \item {\ptt be}, \bold{10}
+  \item {\ptt bes}, \bold{10}
+  \item {\ptt BEST_FIRST}, \bold{29}, 30
+  \item {\ptt Best_tac}, \bold{121}
+  \item {\ptt best_tac}, \bold{119}
+  \item {\ptt beta_conversion}, \bold{41}
+  \item {\ptt bicompose}, \bold{43}
+  \item {\ptt bimatch_tac}, \bold{22}
+  \item {\ptt bind_thm}, 8, \bold{8}, 35
+  \item binders, \bold{72}
+  \item {\ptt biresolution}, \bold{43}
+  \item {\ptt biresolve_tac}, \bold{22}, 121
+  \item {\ptt Blast.depth_tac}, \bold{119}
+  \item {\ptt Blast.trace}, \bold{119}
+  \item {\ptt Blast_tac}, \bold{121}
+  \item {\ptt blast_tac}, \bold{119}
+  \item {\ptt Bound}, \bold{56}, 77, 79, 80
+  \item {\ptt bound_hyp_subst_tac}, \bold{91}
+  \item {\ptt br}, \bold{10}
+  \item {\ptt BREADTH_FIRST}, \bold{29}
+  \item {\ptt brs}, \bold{10}
+  \item {\ptt bw}, \bold{11}
+  \item {\ptt bws}, \bold{11}
+  \item {\ptt by}, \bold{7}, 9, 10, 14
   \item {\ptt byev}, \bold{7}
 
   \indexspace
 
-  \item {\ptt cd}, \bold{3}, 54
-  \item {\ptt cert_axm}, \bold{63}
-  \item {\ptt CHANGED}, \bold{31}
+  \item {\ptt cd}, \bold{2}, 50
+  \item {\ptt cert_axm}, \bold{58}
+  \item {\ptt CHANGED}, \bold{28}
   \item {\ptt chop}, \bold{9}, 13
   \item {\ptt choplev}, \bold{9}
   \item claset
-    \subitem current, 129
-  \item {\ptt claset} ML type, 125
+    \subitem current, 120
+  \item {\ptt claset} ML type, 116
   \item classes
-    \subitem context conditions, 52
-  \item classical reasoner, 121--131
-    \subitem setting up, 130
-    \subitem tactics, 127
-  \item classical sets, 125
-  \item {\ptt ClassicalFun}, 130
-  \item {\ptt combination}, \bold{45}
+    \subitem context conditions, 48
+  \item classical reasoner, 112--122
+    \subitem setting up, 122
+    \subitem tactics, 118
+  \item classical sets, 115
+  \item {\ptt ClassicalFun}, 122
+  \item {\ptt combination}, \bold{41}
   \item {\ptt commit}, \bold{2}
-  \item {\ptt COMP}, \bold{47}
-  \item {\ptt compose}, \bold{47}
-  \item {\ptt compose_tac}, \bold{22}
-  \item {\ptt compSWrapper}, \bold{127}
-  \item {\ptt compWrapper}, \bold{127}
-  \item {\ptt concl_of}, \bold{40}
-  \item {\ptt COND}, \bold{32}
-  \item congruence rules, 105
-  \item {\ptt Const}, \bold{61}, 86, 95
-  \item {\ptt Constant}, 83, 95
-  \item constants, \bold{61}
-    \subitem for translations, 73
-    \subitem syntactic, 88
-  \item {\ptt contr_tac}, \bold{129}
-  \item {\ptt could_unify}, \bold{24}
-  \item {\ptt cterm} ML type, 63
-  \item {\ptt cterm_instantiate}, \bold{39}
-  \item {\ptt cterm_of}, \bold{63}
-  \item {\ptt ctyp}, \bold{64}
-  \item {\ptt ctyp_of}, \bold{65}
-  \item {\ptt cut_facts_tac}, 7, \bold{19}, 100
-  \item {\ptt cut_inst_tac}, \bold{19}
-  \item {\ptt cut_rl} theorem, 21
+  \item {\ptt COMP}, \bold{43}
+  \item {\ptt compose}, \bold{43}
+  \item {\ptt compose_tac}, \bold{21}
+  \item {\ptt compSWrapper}, \bold{118}
+  \item {\ptt compWrapper}, \bold{118}
+  \item {\ptt concl_of}, \bold{37}
+  \item {\ptt COND}, \bold{30}
+  \item congruence rules, 97
+  \item {\ptt Const}, \bold{56}, 79, 88
+  \item {\ptt Constant}, 76, 88
+  \item constants, \bold{56}
+    \subitem for translations, 68
+    \subitem syntactic, 81
+  \item {\ptt contr_tac}, \bold{121}
+  \item {\ptt could_unify}, \bold{23}
+  \item {\ptt cterm} ML type, 58
+  \item {\ptt cterm_instantiate}, \bold{36}
+  \item {\ptt cterm_of}, \bold{58}
+  \item {\ptt ctyp}, \bold{59}
+  \item {\ptt ctyp_of}, \bold{59}
+  \item {\ptt cut_facts_tac}, 7, \bold{18}, 92
+  \item {\ptt cut_inst_tac}, \bold{18}
+  \item {\ptt cut_rl} theorem, 19
 
   \indexspace
 
-  \item {\ptt datatype}, 103
-  \item {\ptt Deepen_tac}, \bold{129}
-  \item {\ptt deepen_tac}, \bold{128}
-  \item {\ptt defer_tac}, \bold{20}
-  \item definitions, \see{rewriting, meta-level}{0}, 20, \bold{52}
+  \item {\ptt datatype}, 95
+  \item {\ptt Deepen_tac}, \bold{121}
+  \item {\ptt deepen_tac}, \bold{120}
+  \item {\ptt defer_tac}, \bold{18}
+  \item definitions, \see{rewriting, meta-level}{0}, 18, \bold{48}
     \subitem unfolding, 7, 8
-  \item {\ptt delcongs}, 106
-  \item {\ptt deleqcongs}, 106, 108
-  \item {\ptt delete_tmpfiles}, \bold{53}
-  \item delimiters, \bold{70}, 73, 74, 76
-  \item {\ptt delrules}, \bold{126}
-  \item {\ptt Delsimps}, \bold{103}, 108, 109
-  \item {\ptt delsimps}, 108, 109
-  \item {\ptt dependent_tr'}, 94, \bold{96}
-  \item {\ptt DEPTH_FIRST}, \bold{31}
-  \item {\ptt DEPTH_SOLVE}, \bold{31}
-  \item {\ptt DEPTH_SOLVE_1}, \bold{31}
-  \item {\ptt depth_tac}, \bold{128}
-  \item {\ptt Deriv.drop}, \bold{49}
-  \item {\ptt Deriv.linear}, \bold{49}
-  \item {\ptt Deriv.size}, \bold{49}
-  \item {\ptt Deriv.tree}, \bold{49}
-  \item {\ptt dest_eq}, \bold{100}
-  \item {\ptt dest_state}, \bold{40}
-  \item destruct-resolution, 17
-  \item {\ptt DETERM}, \bold{32}
-  \item discrimination nets, \bold{24}
-  \item {\ptt dmatch_tac}, \bold{17}
-  \item {\ptt dres_inst_tac}, \bold{18}
-  \item {\ptt dresolve_tac}, \bold{17}
-  \item {\ptt dtac}, \bold{19}
-  \item {\ptt dummyT}, 86, 87, 97
+  \item {\ptt delcongs}, 97
+  \item {\ptt deleqcongs}, 97, 100
+  \item {\ptt delete_tmpfiles}, \bold{49}
+  \item delimiters, \bold{65}, 67, 68, 70
+  \item {\ptt delrules}, \bold{116}
+  \item {\ptt Delsimps}, \bold{95}, 99, 100
+  \item {\ptt delsimps}, 99, 100
+  \item {\ptt dependent_tr'}, 86, \bold{88}
+  \item {\ptt DEPTH_FIRST}, \bold{29}
+  \item {\ptt DEPTH_SOLVE}, \bold{29}
+  \item {\ptt DEPTH_SOLVE_1}, \bold{29}
+  \item {\ptt depth_tac}, \bold{120}
+  \item {\ptt Deriv.drop}, \bold{45}
+  \item {\ptt Deriv.linear}, \bold{45}
+  \item {\ptt Deriv.size}, \bold{45}
+  \item {\ptt Deriv.tree}, \bold{45}
+  \item {\ptt dest_eq}, \bold{92}
+  \item {\ptt dest_state}, \bold{37}
+  \item destruct-resolution, 15
+  \item {\ptt DETERM}, \bold{30}
+  \item discrimination nets, \bold{22}
+  \item {\ptt dmatch_tac}, \bold{16}
+  \item {\ptt dres_inst_tac}, \bold{17}
+  \item {\ptt dresolve_tac}, \bold{15}
+  \item {\ptt dtac}, \bold{17}
+  \item {\ptt dummyT}, 79, 80, 89
 
   \indexspace
 
-  \item elim-resolution, 16
-  \item {\ptt ematch_tac}, \bold{17}
-  \item {\ptt empty} constant, 92
-  \item {\ptt empty_cs}, \bold{125}
-  \item {\ptt empty_ss}, 108, 119
-  \item {\ptt eq_assume_tac}, \bold{17}, 125
-  \item {\ptt eq_assumption}, \bold{46}
-  \item {\ptt eq_mp_tac}, \bold{130}
-  \item {\ptt eq_reflection} theorem, \bold{100}, 116
-  \item {\ptt eq_thm}, \bold{32}
-  \item {\ptt equal_elim}, \bold{44}
-  \item {\ptt equal_intr}, \bold{44}
-  \item equality, 98--101
-  \item {\ptt eres_inst_tac}, \bold{18}
-  \item {\ptt eresolve_tac}, \bold{16}
-  \item {\ptt eta_contract}, \bold{4}, 90
-  \item {\ptt etac}, \bold{19}
-  \item {\ptt EVERY}, \bold{29}
-  \item {\ptt EVERY'}, 35
-  \item {\ptt EVERY1}, \bold{36}
+  \item elim-resolution, 15
+  \item {\ptt ematch_tac}, \bold{16}
+  \item {\ptt empty} constant, 85
+  \item {\ptt empty_cs}, \bold{116}
+  \item {\ptt empty_ss}, 100, 110
+  \item {\ptt eq_assume_tac}, \bold{16}, 116
+  \item {\ptt eq_assumption}, \bold{43}
+  \item {\ptt eq_mp_tac}, \bold{121}
+  \item {\ptt eq_reflection} theorem, \bold{92}, 107
+  \item {\ptt eq_thm}, \bold{30}
+  \item {\ptt equal_elim}, \bold{41}
+  \item {\ptt equal_intr}, \bold{40}
+  \item equality, 90--93
+  \item {\ptt eres_inst_tac}, \bold{17}
+  \item {\ptt eresolve_tac}, \bold{15}
+  \item {\ptt eta_contract}, \bold{4}, 83
+  \item {\ptt etac}, \bold{17}
+  \item {\ptt EVERY}, \bold{27}
+  \item {\ptt EVERY'}, 33
+  \item {\ptt EVERY1}, \bold{33}
   \item examples
-    \subitem of logic definitions, 79
-    \subitem of macros, 92, 93
-    \subitem of mixfix declarations, 75
-    \subitem of simplification, 109
-    \subitem of translations, 96
+    \subitem of logic definitions, 73
+    \subitem of macros, 85, 86
+    \subitem of mixfix declarations, 70
+    \subitem of simplification, 101
+    \subitem of translations, 88
   \item exceptions
     \subitem printing of, 4
   \item {\ptt expandshort} shell script, 5
   \item {\ptt exportML}, \bold{2}
-  \item {\ptt extensional}, \bold{45}
+  \item {\ptt extensional}, \bold{41}
 
   \indexspace
 
   \item {\ptt fa}, \bold{11}
-  \item {\ptt Fast_tac}, \bold{129}
-  \item {\ptt fast_tac}, \bold{127}
+  \item {\ptt Fast_tac}, \bold{121}
+  \item {\ptt fast_tac}, \bold{119}
   \item {\ptt fd}, \bold{11}
   \item {\ptt fds}, \bold{11}
   \item {\ptt fe}, \bold{11}
   \item {\ptt fes}, \bold{11}
   \item files
-    \subitem reading, 2, 53
-  \item {\ptt filt_resolve_tac}, \bold{24}
-  \item {\ptt FILTER}, \bold{30}
-  \item {\ptt filter_goal}, \bold{15}
-  \item {\ptt filter_thms}, \bold{25}
+    \subitem reading, 2, 49
+  \item {\ptt filt_resolve_tac}, \bold{23}
+  \item {\ptt FILTER}, \bold{28}
+  \item {\ptt filter_goal}, \bold{14}
+  \item {\ptt filter_thms}, \bold{23}
   \item {\ptt findE}, \bold{9}
   \item {\ptt findEs}, \bold{9}
-  \item {\ptt findI}, \bold{9}
-  \item {\ptt finish_html}, \bold{59}
-  \item {\ptt FIRST}, \bold{29}
-  \item {\ptt FIRST'}, 35
-  \item {\ptt FIRST1}, \bold{36}
-  \item {\ptt FIRSTGOAL}, \bold{34}
-  \item flex-flex constraints, 22, 40, 48
-  \item {\ptt flexflex_rule}, \bold{48}
-  \item {\ptt flexflex_tac}, \bold{22}
-  \item {\ptt fold_goals_tac}, \bold{20}
-  \item {\ptt fold_tac}, \bold{20}
-  \item {\ptt forall_elim}, \bold{45}
-  \item {\ptt forall_elim_list}, \bold{45}
-  \item {\ptt forall_elim_var}, \bold{45}
-  \item {\ptt forall_elim_vars}, \bold{46}
-  \item {\ptt forall_intr}, \bold{45}
-  \item {\ptt forall_intr_frees}, \bold{45}
-  \item {\ptt forall_intr_list}, \bold{45}
-  \item {\ptt force_strip_shyps}, \bold{41}
-  \item {\ptt forw_inst_tac}, \bold{18}
-  \item forward proof, 17, 38
-  \item {\ptt forward_tac}, \bold{17}
+  \item {\ptt findI}, \bold{8}
+  \item {\ptt finish_html}, \bold{54}
+  \item {\ptt FIRST}, \bold{27}
+  \item {\ptt FIRST'}, 33
+  \item {\ptt FIRST1}, \bold{33}
+  \item {\ptt FIRSTGOAL}, \bold{32}
+  \item flex-flex constraints, 20, 37, 44
+  \item {\ptt flexflex_rule}, \bold{44}
+  \item {\ptt flexflex_tac}, \bold{21}
+  \item {\ptt fold_goals_tac}, \bold{19}
+  \item {\ptt fold_tac}, \bold{19}
+  \item {\ptt forall_elim}, \bold{42}
+  \item {\ptt forall_elim_list}, \bold{42}
+  \item {\ptt forall_elim_var}, \bold{42}
+  \item {\ptt forall_elim_vars}, \bold{42}
+  \item {\ptt forall_intr}, \bold{41}
+  \item {\ptt forall_intr_frees}, \bold{42}
+  \item {\ptt forall_intr_list}, \bold{42}
+  \item {\ptt force_strip_shyps}, \bold{37}
+  \item {\ptt forw_inst_tac}, \bold{17}
+  \item forward proof, 15, 16, 35
+  \item {\ptt forward_tac}, \bold{16}
   \item {\ptt fr}, \bold{11}
-  \item {\ptt Free}, \bold{61}, 86
-  \item {\ptt freezeT}, \bold{46}
+  \item {\ptt Free}, \bold{56}, 79
+  \item {\ptt freezeT}, \bold{42}
   \item {\ptt frs}, \bold{11}
-  \item {\ptt Full_simp_tac}, \bold{103}, 108
-  \item {\ptt full_simp_tac}, 108, \bold{109}
-  \item {\ptt fun} type, 64
-  \item function applications, \bold{61}
+  \item {\ptt Full_simp_tac}, \bold{94}, 100
+  \item {\ptt full_simp_tac}, \bold{99}, 100
+  \item {\ptt fun} type, 59
+  \item function applications, \bold{56}
 
   \indexspace
 
-  \item {\ptt get_axiom}, \bold{56}
-  \item {\ptt get_thm}, \bold{56}
-  \item {\ptt getgoal}, \bold{15}
-  \item {\ptt gethyps}, \bold{15}, 34
+  \item {\ptt get_axiom}, \bold{51}
+  \item {\ptt get_thm}, \bold{51}
+  \item {\ptt getgoal}, \bold{14}
+  \item {\ptt gethyps}, \bold{14}, 31
   \item {\ptt goal}, \bold{7}, 13
   \item {\ptt goals_limit}, \bold{10}
   \item {\ptt goalw}, \bold{7}
@@ -298,502 +302,505 @@
 
   \indexspace
 
-  \item {\ptt has_fewer_prems}, \bold{32}
-  \item HTML, \bold{57}
-  \item {\ptt hyp_subst_tac}, \bold{99}
-  \item {\ptt hyp_subst_tacs}, \bold{131}
-  \item {\ptt HypsubstFun}, 100, 131
+  \item {\ptt has_fewer_prems}, \bold{30}
+  \item HTML, \bold{53}
+  \item {\ptt hyp_subst_tac}, \bold{91}
+  \item {\ptt hyp_subst_tacs}, \bold{122}
+  \item {\ptt HypsubstFun}, 92, 122
 
   \indexspace
 
-  \item {\ptt id} nonterminal, \bold{70}, 84, 91
-  \item identifiers, 70
-  \item {\ptt idt} nonterminal, 91
-  \item {\ptt idts} nonterminal, \bold{70}, 78
-  \item {\ptt IF_UNSOLVED}, \bold{32}
-  \item {\ptt iff_reflection} theorem, 116
-  \item {\ptt imp_intr} theorem, \bold{100}
-  \item {\ptt implies_elim}, \bold{44}
-  \item {\ptt implies_elim_list}, \bold{44}
-  \item {\ptt implies_intr}, \bold{43}
-  \item {\ptt implies_intr_hyps}, \bold{44}
-  \item {\ptt implies_intr_list}, \bold{43}
-  \item {\ptt incr_boundvars}, \bold{62}, 96
-  \item {\ptt indexname} ML type, 61, 71
-  \item infixes, \bold{77}
-  \item {\ptt init_html}, \bold{58}
-  \item {\ptt insert} constant, 92
-  \item {\ptt inst_step_tac}, \bold{128}
-  \item {\ptt instantiate}, \bold{46}
-  \item instantiation, 17, 39, 46
-  \item {\ptt INTLEAVE}, \bold{28}, 30
-  \item {\ptt INTLEAVE'}, 35
-  \item {\ptt invoke_oracle}, \bold{65}
-  \item {\ptt is} nonterminal, 93
+  \item {\ptt id} nonterminal, \bold{65}, 77, 84
+  \item identifiers, 65
+  \item {\ptt idt} nonterminal, 83
+  \item {\ptt idts} nonterminal, \bold{65}, 72
+  \item {\ptt IF_UNSOLVED}, \bold{30}
+  \item {\ptt iff_reflection} theorem, 107
+  \item {\ptt imp_intr} theorem, \bold{92}
+  \item {\ptt implies_elim}, \bold{40}
+  \item {\ptt implies_elim_list}, \bold{40}
+  \item {\ptt implies_intr}, \bold{40}
+  \item {\ptt implies_intr_hyps}, \bold{40}
+  \item {\ptt implies_intr_list}, \bold{40}
+  \item {\ptt incr_boundvars}, \bold{57}, 88
+  \item {\ptt indexname} ML type, 56, 66
+  \item infixes, \bold{71}
+  \item {\ptt init_html}, \bold{54}
+  \item {\ptt insert} constant, 85
+  \item {\ptt inst_step_tac}, \bold{120}
+  \item {\ptt instantiate}, \bold{42}
+  \item instantiation, 16, 36, 42
+  \item {\ptt INTLEAVE}, \bold{26}, 27
+  \item {\ptt INTLEAVE'}, 33
+  \item {\ptt invoke_oracle}, \bold{60}
+  \item {\ptt is} nonterminal, 85
 
   \indexspace
 
-  \item {\ptt joinrules}, \bold{130}
+  \item {\ptt joinrules}, \bold{121}
 
   \indexspace
 
-  \item {\ptt keep_derivs}, \bold{49}
+  \item {\ptt keep_derivs}, \bold{45}
 
   \indexspace
 
-  \item $\lambda$-abstractions, 24, \bold{61}
-  \item $\lambda$-calculus, 43, 44, 70
-  \item {\ptt lessb}, \bold{23}
-  \item lexer, \bold{70}
-  \item {\ptt lift_rule}, \bold{47}
-  \item lifting, 47
-  \item {\ptt loadpath}, \bold{53}
-  \item {\ptt logic} class, 70, 75
-  \item {\ptt logic} nonterminal, \bold{70}
-  \item {\ptt Logic.auto_rename}, \bold{21}
-  \item {\ptt Logic.set_rename_prefix}, \bold{21}
-  \item {\ptt loose_bnos}, \bold{62}, 97
+  \item $\lambda$-abstractions, 22, \bold{56}
+  \item $\lambda$-calculus, 39, 41, 65
+  \item {\ptt lessb}, \bold{22}
+  \item lexer, \bold{65}
+  \item {\ptt lift_rule}, \bold{44}
+  \item lifting, 44
+  \item {\ptt loadpath}, \bold{49}
+  \item {\ptt logic} class, 63, 65, 69
+  \item {\ptt logic} nonterminal, \bold{63}
+  \item {\ptt Logic.auto_rename}, \bold{20}
+  \item {\ptt Logic.set_rename_prefix}, \bold{20}
+  \item {\ptt loose_bnos}, \bold{57}, 89
 
   \indexspace
 
-  \item macros, 88--94
+  \item macros, 81--86
   \item {\ptt make-all} shell script, 5
-  \item {\ptt make_elim}, \bold{40}
-  \item {\ptt make_html}, \bold{59}
-  \item {\ptt Match} exception, 95, 100
-  \item {\ptt match_tac}, \bold{17}, 125
-  \item {\ptt max_pri}, 68, \bold{74}
-  \item {\ptt merge_ss}, 108
-  \item {\ptt merge_theories}, \bold{56}, \fnote{81}
-  \item meta-assumptions, 33, 42, 43, 46
+  \item {\ptt make_elim}, \bold{37}, 117
+  \item {\ptt make_html}, \bold{54}
+  \item {\ptt Match} exception, 88, 92
+  \item {\ptt match_tac}, \bold{16}, 116
+  \item {\ptt max_pri}, 63, \bold{69}
+  \item {\ptt merge_ss}, 100
+  \item {\ptt merge_theories}, \bold{52}, \fnote{75}
+  \item meta-assumptions, 31, 39, 40, 43
     \subitem printing of, 3
-  \item meta-equality, 42, 44
-  \item meta-implication, 42, 43
-  \item meta-quantifiers, 43, 45
-  \item meta-rewriting, 7, 12, 13, \bold{20}, 
-		\seealso{tactics, theorems}{132}
-    \subitem in terms, 48
-    \subitem in theorems, 39
-  \item meta-rules, \see{meta-rules}{0}, 42--48
-  \item {\ptt METAHYPS}, 15, \bold{33}
-  \item mixfix declarations, 51, 73--78
-  \item {\ptt mk_case_split_tac}, \bold{119}
-  \item {\ptt ML} section, 52, 95, 96
-  \item {\ptt mp} theorem, \bold{130}
-  \item {\ptt mp_tac}, \bold{129}
-  \item {\ptt MRL}, \bold{38}
-  \item {\ptt MRS}, \bold{38}
+  \item meta-equality, 39--41
+  \item meta-implication, 39, 40
+  \item meta-quantifiers, 40, 41
+  \item meta-rewriting, 7, 11, 12, \bold{18}, 
+		\seealso{tactics, theorems}{123}
+    \subitem in terms, 44
+    \subitem in theorems, 35
+  \item meta-rules, \see{meta-rules}{0}, 39--44
+  \item {\ptt METAHYPS}, 14, \bold{31}
+  \item mixfix declarations, 47, 68--72
+  \item {\ptt mk_case_split_tac}, \bold{111}
+  \item {\ptt ML} section, 48, 87, 89
+  \item {\ptt mp} theorem, \bold{122}
+  \item {\ptt mp_tac}, \bold{121}
+  \item {\ptt MRL}, \bold{35}
+  \item {\ptt MRS}, \bold{35}
 
   \indexspace
 
-  \item name tokens, \bold{70}
-  \item {\ptt net_bimatch_tac}, \bold{24}
-  \item {\ptt net_biresolve_tac}, \bold{24}
-  \item {\ptt net_match_tac}, \bold{24}
-  \item {\ptt net_resolve_tac}, \bold{24}
-  \item {\ptt no_tac}, \bold{30}
-  \item {\ptt None}, \bold{26}
-  \item {\ptt not_elim} theorem, \bold{130}
-  \item {\ptt nprems_of}, \bold{40}
-  \item numerals, 70
+  \item name tokens, \bold{65}
+  \item {\ptt net_bimatch_tac}, \bold{23}
+  \item {\ptt net_biresolve_tac}, \bold{23}
+  \item {\ptt net_match_tac}, \bold{23}
+  \item {\ptt net_resolve_tac}, \bold{22}
+  \item {\ptt no_tac}, \bold{27}
+  \item {\ptt None}, \bold{24}
+  \item {\ptt not_elim} theorem, \bold{122}
+  \item {\ptt nprems_of}, \bold{37}
+  \item numerals, 65
 
   \indexspace
 
-  \item {\ptt o} type, 79
-  \item {\ptt op} symbol, 77
-  \item {\ptt option} ML type, 26
-  \item oracles, 65--66
-  \item {\ptt ORELSE}, \bold{28}, 30, 34
-  \item {\ptt ORELSE'}, 35
+  \item {\ptt o} type, 73
+  \item {\ptt op} symbol, 71
+  \item {\ptt option} ML type, 24
+  \item oracles, 60--61
+  \item {\ptt ORELSE}, \bold{26}, 27, 28, 32
+  \item {\ptt ORELSE'}, 33
 
   \indexspace
 
   \item parameters
-    \subitem removing unused, 22
-    \subitem renaming, 12, 21, 48
-  \item {\ptt parents_of}, \bold{57}
-  \item parse trees, 83
-  \item {\ptt parse_ast_translation}, 95
-  \item {\ptt parse_rules}, 90
-  \item {\ptt parse_translation}, 95
-  \item {\ptt pause_tac}, \bold{26}
-  \item Poly/{\ML} compiler, 1, 2, 4, 55
-  \item {\ptt pop_proof}, \bold{14}
+    \subitem removing unused, 20
+    \subitem renaming, 11, 19, 44
+  \item {\ptt parents_of}, \bold{52}
+  \item parse trees, 76
+  \item {\ptt parse_ast_translation}, 87
+  \item {\ptt parse_rules}, 83
+  \item {\ptt parse_translation}, 87
+  \item {\ptt pause_tac}, \bold{24}
+  \item Poly/{\ML} compiler, 1, 2, 4, 50
+  \item {\ptt pop_proof}, \bold{13}
   \item {\ptt pr}, \bold{10}
-  \item {\ptt premises}, \bold{7}, 14
-  \item {\ptt prems_of}, \bold{40}
-  \item {\ptt prems_of_ss}, 108
-  \item pretty printing, 74, 76--77, 93
+  \item {\ptt premises}, \bold{7}, 13
+  \item {\ptt prems_of}, \bold{37}
+  \item {\ptt prems_of_ss}, 100
+  \item pretty printing, 68, 71, 85
   \item {\ptt Pretty.setdepth}, \bold{3}
   \item {\ptt Pretty.setmargin}, \bold{3}
-  \item {\ptt PRIMITIVE}, \bold{25}
-  \item {\ptt primrec}, 103
-  \item {\ptt prin}, 5, \bold{14}
-  \item {\ptt print_ast_translation}, 95
-  \item {\ptt print_cs}, \bold{125}
+  \item {\ptt PRIMITIVE}, \bold{24}
+  \item {\ptt primrec}, 95
+  \item {\ptt prin}, 4, \bold{14}
+  \item {\ptt print_ast_translation}, 87
+  \item {\ptt print_cs}, \bold{116}
   \item {\ptt print_depth}, \bold{3}
-  \item {\ptt print_exn}, \bold{4}, 37
-  \item {\ptt print_goals}, \bold{38}
-  \item {\ptt print_rules}, 90
-  \item {\ptt print_syntax}, \bold{72}
-  \item {\ptt print_tac}, \bold{26}
-  \item {\ptt print_theory}, \bold{57}
-  \item {\ptt print_thm}, \bold{38}
-  \item {\ptt print_translation}, 95
+  \item {\ptt print_exn}, \bold{4}, 34
+  \item {\ptt print_goals}, \bold{35}
+  \item {\ptt print_rules}, 83
+  \item {\ptt print_syntax}, \bold{66}
+  \item {\ptt print_tac}, \bold{24}
+  \item {\ptt print_theory}, \bold{52}
+  \item {\ptt print_thm}, \bold{35}
+  \item {\ptt print_translation}, 87
   \item printing control, 3--4
   \item {\ptt printyp}, \bold{14}
-  \item priorities, 67, \bold{74}
-  \item priority grammars, 67--68
+  \item priorities, 62, \bold{69}
+  \item priority grammars, 62--63
   \item {\ptt prlev}, \bold{10}
   \item {\ptt prlim}, \bold{10}
-  \item productions, 67, 73, 74
-    \subitem copy, \bold{73}, 74, 85
-  \item {\ptt proof} ML type, 14
-  \item proof objects, 48--49
+  \item productions, 62, 67, 68
+    \subitem copy, \bold{67}, 68, 77
+  \item {\ptt proof} ML type, 13
+  \item proof objects, 44--45
   \item proof state, 6
-    \subitem printing of, 10
+    \subitem printing of, 9
   \item {\ptt proof_timing}, \bold{10}
-  \item proofs, 6--15
-    \subitem inspecting the state, 15
-    \subitem managing multiple, 13
-    \subitem saving and restoring, 14
+  \item proofs, 6--14
+    \subitem inspecting the state, 14
+    \subitem managing multiple, 12
+    \subitem saving and restoring, 13
     \subitem stacking, 13
     \subitem starting, 6
     \subitem timing, 10
-  \item {\ptt PROP} symbol, 69
-  \item {\ptt prop} nonterminal, \bold{68}, 79
-  \item {\ptt prop} type, 64, 70
+  \item {\ptt PROP} symbol, 64
+  \item {\ptt prop} nonterminal, \bold{63}, 73
+  \item {\ptt prop} type, 59, 63
   \item {\ptt prove_goal}, 10, \bold{12}
-  \item {\ptt prove_goalw}, \bold{13}
-  \item {\ptt prove_goalw_cterm}, \bold{13}
-  \item {\ptt prth}, \bold{37}
-  \item {\ptt prthq}, \bold{38}
-  \item {\ptt prths}, \bold{38}
-  \item {\ptt prune_params_tac}, \bold{22}
-  \item {\ptt Pure} theory, 50, 68, 72
-  \item {\ptt pure_thy}, \bold{56}
-  \item {\ptt push_proof}, \bold{14}
-  \item {\ptt pwd}, \bold{3}
+  \item {\ptt prove_goalw}, \bold{12}
+  \item {\ptt prove_goalw_cterm}, \bold{12}
+  \item {\ptt prth}, \bold{34}
+  \item {\ptt prthq}, \bold{35}
+  \item {\ptt prths}, \bold{34}
+  \item {\ptt prune_params_tac}, \bold{21}
+  \item {\ptt Pure} theory, 46, 63, 67
+  \item {\ptt pure_thy}, \bold{52}
+  \item {\ptt push_proof}, \bold{13}
+  \item {\ptt pwd}, \bold{2}
 
   \indexspace
 
-  \item {\ptt qed}, \bold{8}, 9
-  \item {\ptt qed_goal}, \bold{13}
-  \item {\ptt qed_goalw}, \bold{13}
-  \item quantifiers, 78
+  \item {\ptt qed}, 8, \bold{8}
+  \item {\ptt qed_goal}, \bold{12}
+  \item {\ptt qed_goalw}, \bold{12}
+  \item quantifiers, 72
   \item {\ptt quit}, \bold{2}
 
   \indexspace
 
   \item {\ptt read}, \bold{14}
-  \item {\ptt read_axm}, \bold{63}
-  \item {\ptt read_cterm}, \bold{63}
-  \item {\ptt read_instantiate}, \bold{39}
-  \item {\ptt read_instantiate_sg}, \bold{39}
+  \item {\ptt read_axm}, \bold{58}
+  \item {\ptt read_cterm}, \bold{58}
+  \item {\ptt read_instantiate}, \bold{36}
+  \item {\ptt read_instantiate_sg}, \bold{36}
   \item reading
-    \subitem axioms, \see{{\tt assume_ax}}{50}
+    \subitem axioms, \see{{\tt assume_ax}}{46}
     \subitem goals, \see{proofs, starting}{6}
-  \item {\ptt reflexive}, \bold{44}
-  \item {\ptt ren}, \bold{12}
-  \item {\ptt rename_last_tac}, \bold{21}
-  \item {\ptt rename_params_rule}, \bold{47}
-  \item {\ptt rename_tac}, \bold{21}
-  \item {\ptt rep_cterm}, \bold{63}
-  \item {\ptt rep_ctyp}, \bold{65}
-  \item {\ptt rep_ss}, 108
-  \item {\ptt rep_thm}, \bold{41}
-  \item {\ptt REPEAT}, \bold{29, 30}
-  \item {\ptt REPEAT1}, \bold{29}
-  \item {\ptt REPEAT_DETERM}, \bold{29}
-  \item {\ptt REPEAT_FIRST}, \bold{35}
-  \item {\ptt REPEAT_SOME}, \bold{34}
-  \item {\ptt res_inst_tac}, \bold{18}, 22
-  \item reserved words, 70, 93
-  \item resolution, 38, 46
-    \subitem tactics, 16
-    \subitem without lifting, 47
-  \item {\ptt resolve_tac}, \bold{16}, 125
-  \item {\ptt restore_proof}, \bold{14}
-  \item {\ptt result}, \bold{8}, 15, 56
-  \item {\ptt rev_mp} theorem, \bold{100}
-  \item rewrite rules, 104--105
-    \subitem permutative, 113--116
-  \item {\ptt rewrite_cterm}, \bold{48}
-  \item {\ptt rewrite_goals_rule}, \bold{39}
-  \item {\ptt rewrite_goals_tac}, \bold{20}, 39
-  \item {\ptt rewrite_rule}, \bold{39}
-  \item {\ptt rewrite_tac}, 8, \bold{20}
+  \item {\ptt reflexive}, \bold{41}
+  \item {\ptt ren}, \bold{11}
+  \item {\ptt rename_last_tac}, \bold{20}
+  \item {\ptt rename_params_rule}, \bold{44}
+  \item {\ptt rename_tac}, \bold{20}
+  \item {\ptt rep_cterm}, \bold{58}
+  \item {\ptt rep_ctyp}, \bold{59}
+  \item {\ptt rep_ss}, 100
+  \item {\ptt rep_thm}, \bold{37}
+  \item {\ptt REPEAT}, \bold{27, 28}
+  \item {\ptt REPEAT1}, \bold{27}
+  \item {\ptt REPEAT_DETERM}, \bold{27}
+  \item {\ptt REPEAT_FIRST}, \bold{32}
+  \item {\ptt REPEAT_SOME}, \bold{32}
+  \item {\ptt res_inst_tac}, \bold{17}, 21
+  \item reserved words, 65, 86
+  \item resolution, 35, 43
+    \subitem tactics, 15
+    \subitem without lifting, 43
+  \item {\ptt resolve_tac}, \bold{15}, 116
+  \item {\ptt restore_proof}, \bold{13}
+  \item {\ptt result}, \bold{8}, 14, 52
+  \item {\ptt rev_mp} theorem, \bold{92}
+  \item rewrite rules, 96--97
+    \subitem permutative, 104--107
+  \item {\ptt rewrite_cterm}, \bold{44}
+  \item {\ptt rewrite_goals_rule}, \bold{36}
+  \item {\ptt rewrite_goals_tac}, \bold{19}, 36
+  \item {\ptt rewrite_rule}, \bold{36}
+  \item {\ptt rewrite_tac}, 8, \bold{19}
   \item rewriting
     \subitem object-level, \see{simplification}{0}
-    \subitem ordered, 113
-    \subitem syntactic, 88--94
-  \item {\ptt rewtac}, \bold{19}
-  \item {\ptt RL}, \bold{38}
-  \item {\ptt RLN}, \bold{38}
-  \item {\ptt rotate_proof}, \bold{14}
-  \item {\ptt rotate_tac}, \bold{22}
-  \item {\ptt RS}, \bold{38}
-  \item {\ptt RSN}, \bold{38}
-  \item {\ptt rtac}, \bold{19}
-  \item {\ptt rule_by_tactic}, 22, \bold{40}
+    \subitem ordered, 104
+    \subitem syntactic, 81--86
+  \item {\ptt rewtac}, \bold{18}
+  \item {\ptt RL}, \bold{35}
+  \item {\ptt RLN}, \bold{35}
+  \item {\ptt rotate_proof}, \bold{13}
+  \item {\ptt rotate_tac}, \bold{20}
+  \item {\ptt RS}, \bold{35}
+  \item {\ptt RSN}, \bold{35}
+  \item {\ptt rtac}, \bold{17}
+  \item {\ptt rule_by_tactic}, 21, \bold{37}
   \item rules
-    \subitem converting destruction to elimination, 40
+    \subitem converting destruction to elimination, 37
 
   \indexspace
 
-  \item {\ptt safe_asm_full_simp_tac}, \bold{107}, 108
-  \item {\ptt safe_step_tac}, 126, \bold{128}
-  \item {\ptt safe_tac}, \bold{128}
-  \item {\ptt save_proof}, \bold{14}
+  \item {\ptt safe_asm_full_simp_tac}, \bold{98}, 100
+  \item {\ptt safe_step_tac}, 117, \bold{120}
+  \item {\ptt safe_tac}, \bold{120}
+  \item {\ptt save_proof}, \bold{13}
   \item saving your work, \bold{1}
-  \item search, 28
-    \subitem tacticals, 30--32
-  \item {\ptt SELECT_GOAL}, 20, \bold{33}
-  \item {\ptt Sequence.seq} ML type, 25
-  \item sequences (lazy lists), \bold{26}
-  \item sequent calculus, 121
+  \item search, 26
+    \subitem tacticals, 28--30
+  \item {\ptt SELECT_GOAL}, 19, \bold{30}
+  \item {\ptt Sequence.seq} ML type, 23
+  \item sequences (lazy lists), \bold{24}
+  \item sequent calculus, 112
   \item sessions, 1--5
-  \item {\ptt set_current_thy}, 104
-  \item {\ptt set_oracle}, \bold{65}
-  \item {\ptt setloop}, 107, 108
-  \item {\ptt setmksimps}, 105, 108, 119
-  \item {\ptt setSolver}, 107, 108, 119
-  \item {\ptt setSSolver}, 107, 108, 119
-  \item {\ptt setsubgoaler}, 106, 108, 119
-  \item {\ptt setSWrapper}, \bold{127}
-  \item {\ptt setWrapper}, \bold{127}
-  \item shell scripts, \bold{5}
+  \item {\ptt set_current_thy}, 96
+  \item {\ptt set_oracle}, \bold{60}
+  \item {\ptt setloop}, 99, 100
+  \item {\ptt setmksimps}, 96, 100, 110
+  \item {\ptt setSolver}, 98, 100, 110
+  \item {\ptt setSSolver}, 98, 100, 110
+  \item {\ptt setsubgoaler}, 98, 100, 110
+  \item {\ptt setSWrapper}, \bold{118}
+  \item {\ptt setWrapper}, \bold{118}
+  \item shell scripts, \bold{4}
   \item shortcuts
-    \subitem for tactics, 18
+    \subitem for tactics, 17
     \subitem for {\tt by} commands, 10
-  \item {\ptt show_brackets}, \bold{4}
-  \item {\ptt show_hyps}, \bold{4}
-  \item {\ptt show_sorts}, \bold{4}, 87
-  \item {\ptt show_types}, \bold{4}, 87, 91, 97
-  \item {\ptt Sign.cterm_of}, 7, 13
-  \item {\ptt Sign.sg} ML type, 50
-  \item {\ptt Sign.string_of_term}, \bold{63}
-  \item {\ptt Sign.string_of_typ}, \bold{64}
-  \item {\ptt sign_of}, 7, 13, \bold{57}
-  \item signatures, \bold{50}, 57, 62, 63, 65
-  \item {\ptt Simp_tac}, \bold{102}, 108
-  \item {\ptt simp_tac}, 108, \bold{109}
-  \item simplification, 102--120
-    \subitem from classical reasoner, 126
-    \subitem setting up, 116
-    \subitem tactics, 109
-  \item simplification sets, 104
+  \item {\ptt show_brackets}, \bold{3}
+  \item {\ptt show_hyps}, \bold{3}
+  \item {\ptt show_sorts}, \bold{3}, 80
+  \item {\ptt show_types}, \bold{3}, 80, 83, 89
+  \item {\ptt Sign.cterm_of}, 7, 12
+  \item {\ptt Sign.sg} ML type, 46
+  \item {\ptt Sign.string_of_term}, \bold{58}
+  \item {\ptt Sign.string_of_typ}, \bold{59}
+  \item {\ptt sign_of}, 7, 12, \bold{52}
+  \item signatures, \bold{46}, 53, 57--59
+  \item {\ptt Simp_tac}, \bold{94}, 100
+  \item {\ptt simp_tac}, \bold{99}, 100
+  \item simplification, 94--111
+    \subitem from classical reasoner, 117
+    \subitem setting up, 107
+    \subitem tactics, 99
+  \item simplification sets, 96
   \item simpset
-    \subitem current, 102, 104, 109
-  \item {\ptt simpset}, 108
-  \item {\ptt simpset} ML type, 108
-  \item {\tt simpset} ML value, 104
-  \item {\ptt simpset_of}, 109
-  \item {\ptt size_of_thm}, 31, \bold{32}, 131
-  \item {\ptt sizef}, \bold{131}
-  \item {\ptt slow_best_tac}, \bold{128}
-  \item {\ptt slow_step_tac}, 126, \bold{129}
-  \item {\ptt slow_tac}, \bold{128}
-  \item {\ptt Some}, \bold{26}
-  \item {\ptt SOMEGOAL}, \bold{34}
-  \item {\ptt sort} nonterminal, \bold{70}
-  \item sort constraints, 69
-  \item sort hypotheses, 41
+    \subitem current, 94, 96, 99
+  \item {\ptt simpset}, 100
+  \item {\ptt simpset} ML type, 100
+  \item {\tt simpset} ML value, 96
+  \item {\ptt simpset_of}, 101
+  \item {\ptt size_of_thm}, 29, \bold{30}, 122
+  \item {\ptt sizef}, \bold{122}
+  \item {\ptt slow_best_tac}, \bold{119}
+  \item {\ptt slow_step_tac}, 117, \bold{120}
+  \item {\ptt slow_tac}, \bold{119}
+  \item {\ptt Some}, \bold{24}
+  \item {\ptt SOMEGOAL}, \bold{32}
+  \item {\ptt sort} nonterminal, \bold{65}
+  \item sort constraints, 64
+  \item sort hypotheses, 37
   \item sorts
     \subitem printing of, 3
-  \item {\ptt split_tac}, \bold{119}
-  \item {\ptt ssubst} theorem, \bold{98}
-  \item {\ptt stac}, \bold{99}
-  \item stamps, 40, \bold{50}, 57
-  \item {\ptt stamps_of_thm}, \bold{40}
-  \item {\ptt stamps_of_thy}, \bold{57}
-  \item {\ptt standard}, \bold{40}
+  \item {\ptt split_tac}, \bold{111}
+  \item {\ptt ssubst} theorem, \bold{90}
+  \item {\ptt stac}, \bold{91}
+  \item stamps, 37, \bold{46}, 53
+  \item {\ptt stamps_of_thm}, \bold{37}
+  \item {\ptt stamps_of_thy}, \bold{53}
+  \item {\ptt standard}, \bold{36}
   \item starting up, \bold{1}
-  \item {\ptt STATE}, \bold{25}
-  \item {\ptt Step_tac}, \bold{129}
-  \item {\ptt step_tac}, 126, \bold{128}
+  \item {\ptt STATE}, \bold{24}
+  \item {\ptt Step_tac}, \bold{121}
+  \item {\ptt step_tac}, 117, \bold{120}
   \item {\ptt store_thm}, \bold{8}
-  \item {\ptt string_of_cterm}, \bold{63}
-  \item {\ptt string_of_ctyp}, \bold{64}
-  \item {\ptt string_of_thm}, \bold{38}
-  \item strings, 70
-  \item {\ptt SUBGOAL}, \bold{25}
-  \item subgoal module, 6--15
-  \item {\ptt subgoal_tac}, \bold{19}
-  \item {\ptt subgoals_of_brl}, \bold{23}
-  \item {\ptt subgoals_tac}, \bold{19}
-  \item {\ptt subst} theorem, 98, \bold{100}
+  \item {\ptt string_of_cterm}, \bold{58}
+  \item {\ptt string_of_ctyp}, \bold{59}
+  \item {\ptt string_of_thm}, \bold{35}
+  \item strings, 65
+  \item {\ptt SUBGOAL}, \bold{24}
+  \item subgoal module, 6--14
+  \item {\ptt subgoal_tac}, \bold{18}
+  \item {\ptt subgoals_of_brl}, \bold{22}
+  \item {\ptt subgoals_tac}, \bold{18}
+  \item {\ptt subst} theorem, 90, \bold{92}
   \item substitution
-    \subitem rules, 98
-  \item {\ptt swap} theorem, \bold{130}
-  \item {\ptt swap_res_tac}, \bold{130}
-  \item {\ptt swapify}, \bold{130}
-  \item {\ptt sym} theorem, 99, \bold{100}
-  \item {\ptt symmetric}, \bold{44}
-  \item {\ptt syn_of}, \bold{72}
+    \subitem rules, 90
+  \item {\ptt swap} theorem, \bold{122}
+  \item {\ptt swap_res_tac}, \bold{121}
+  \item {\ptt swapify}, \bold{121}
+  \item {\ptt sym} theorem, 91, \bold{92}
+  \item {\ptt symmetric}, \bold{41}
+  \item {\ptt syn_of}, \bold{66}
   \item syntax
-    \subitem Pure, 68--73
-    \subitem transformations, 83--97
-  \item {\ptt syntax} section, 51
-  \item {\ptt Syntax.ast} ML type, 83
-  \item {\ptt Syntax.print_gram}, \bold{72}
-  \item {\ptt Syntax.print_syntax}, \bold{72}
-  \item {\ptt Syntax.print_trans}, \bold{72}
-  \item {\ptt Syntax.stat_norm_ast}, 92
-  \item {\ptt Syntax.syntax} ML type, 72
-  \item {\ptt Syntax.test_read}, 76, 92
-  \item {\ptt Syntax.trace_norm_ast}, 92
+    \subitem Pure, 63--68
+    \subitem transformations, 76--89
+  \item {\ptt syntax} section, 47
+  \item {\ptt Syntax.ast} ML type, 76
+  \item {\ptt Syntax.print_gram}, \bold{67}
+  \item {\ptt Syntax.print_syntax}, \bold{66}
+  \item {\ptt Syntax.print_trans}, \bold{67}
+  \item {\ptt Syntax.stat_norm_ast}, 84
+  \item {\ptt Syntax.syntax} ML type, 66
+  \item {\ptt Syntax.test_read}, 70, 84
+  \item {\ptt Syntax.trace_norm_ast}, 84
 
   \indexspace
 
-  \item {\ptt Tactic}, \bold{25}
-  \item {\ptt tactic} ML type, 16
-  \item tacticals, 28--36
-    \subitem conditional, 32
-    \subitem deterministic, 32
-    \subitem for filtering, 30
-    \subitem for restriction to a subgoal, 33
-    \subitem identities for, 29
-    \subitem joining a list of tactics, 29
-    \subitem joining tactic functions, 35
-    \subitem joining two tactics, 28
-    \subitem repetition, 29
-    \subitem scanning for subgoals, 34
-    \subitem searching, 31
-  \item tactics, 16--27
-    \subitem assumption, \bold{17}, 18
+  \item {\ptt Tactic}, \bold{24}
+  \item {\ptt tactic} ML type, 15
+  \item tacticals, 26--33
+    \subitem conditional, 29
+    \subitem deterministic, 29
+    \subitem for filtering, 28
+    \subitem for restriction to a subgoal, 30
+    \subitem identities for, 27
+    \subitem joining a list of tactics, 26
+    \subitem joining tactic functions, 32, 33
+    \subitem joining two tactics, 26
+    \subitem repetition, 27
+    \subitem scanning for subgoals, 31
+    \subitem searching, 28, 29
+  \item tactics, 15--25
+    \subitem assumption, \bold{16}, 17
     \subitem commands for applying, 7
-    \subitem debugging, 14
-    \subitem filtering results of, 30
-    \subitem for composition, 22
-    \subitem for contradiction, 129
-    \subitem for inserting facts, 19
-    \subitem for Modus Ponens, 129
-    \subitem instantiation, 17
-    \subitem matching, 17
-    \subitem meta-rewriting, 18, \bold{20}
-    \subitem primitives for coding, 25
-    \subitem resolution, \bold{16}, 18, 23, 24
-    \subitem restricting to a subgoal, 33
-    \subitem simplification, 109
-    \subitem substitution, 98--101
-    \subitem tracing, 26
-  \item {\ptt tapply}, \bold{25}
+    \subitem debugging, 13
+    \subitem filtering results of, 28
+    \subitem for composition, 21
+    \subitem for contradiction, 121
+    \subitem for inserting facts, 18
+    \subitem for Modus Ponens, 121
+    \subitem instantiation, 16
+    \subitem matching, 16
+    \subitem meta-rewriting, 17, \bold{18}
+    \subitem primitives for coding, 23
+    \subitem resolution, \bold{15}, 17, 21, 22
+    \subitem restricting to a subgoal, 30
+    \subitem simplification, 99
+    \subitem substitution, 90--93
+    \subitem tracing, 24
+  \item {\ptt tapply}, \bold{23}
   \item {\ptt teeinput} shell script, 5
-  \item {\ptt TERM}, 63
-  \item {\ptt term} ML type, 61, 86
-  \item terms, \bold{61}
-    \subitem certified, \bold{62}
-    \subitem made from ASTs, 85
-    \subitem printing of, 14, 63
+  \item {\ptt TERM}, 58
+  \item {\ptt term} ML type, 56, 79
+  \item terms, \bold{56}
+    \subitem certified, \bold{57}
+    \subitem made from ASTs, 79
+    \subitem printing of, 14, 58
     \subitem reading of, 14
-  \item {\ptt TFree}, \bold{64}
-  \item {\ptt THEN}, \bold{28}, 30, 34
-  \item {\ptt THEN'}, 35
-  \item {\ptt THEN_BEST_FIRST}, \bold{32}
-  \item theorems, 37--49
-    \subitem equality of, 32
-    \subitem extracting, 56
+  \item {\ptt TFree}, \bold{59}
+  \item {\ptt THEN}, \bold{26}, 27, 32
+  \item {\ptt THEN'}, 33
+  \item {\ptt THEN_BEST_FIRST}, \bold{29}
+  \item theorems, 34--45
+    \subitem equality of, 30
+    \subitem extracting, 51
     \subitem extracting proved, 8
-    \subitem joining by resolution, 38
-    \subitem of pure theory, 20
-    \subitem printing of, 37
-    \subitem retrieving, 9
-    \subitem size of, 32
-    \subitem standardizing, 39
+    \subitem joining by resolution, 35
+    \subitem of pure theory, 19
+    \subitem printing of, 34
+    \subitem retrieving, 8
+    \subitem size of, 30
+    \subitem standardizing, 36
     \subitem storing, 8
-    \subitem taking apart, 40
-  \item theories, 50--66
-    \subitem axioms of, 56
-    \subitem constructing, \bold{56}
-    \subitem inspecting, \bold{57}
-    \subitem loading, 53
-    \subitem parent, \bold{50}
-    \subitem pseudo, \bold{55}
-    \subitem reloading, \bold{54}
-    \subitem removing, \bold{54}
-    \subitem theorems of, 56
-  \item {\ptt THEORY} exception, 50, 56
-  \item {\ptt theory} ML type, 50
-  \item {\ptt theory_of_thm}, \bold{40}
-  \item {\ptt thin_tac}, \bold{22}
-  \item {\ptt THM} exception, 37, 38, 42, 47
-  \item {\ptt thm} ML type, 37
+    \subitem taking apart, 37
+  \item theories, 46--61
+    \subitem axioms of, 51
+    \subitem constructing, \bold{52}
+    \subitem inspecting, \bold{52}
+    \subitem loading, 49
+    \subitem parent, \bold{46}
+    \subitem pseudo, \bold{50}
+    \subitem reloading, \bold{50}
+    \subitem removing, \bold{50}
+    \subitem theorems of, 51
+  \item {\ptt THEORY} exception, 46, 51
+  \item {\ptt theory} ML type, 46
+  \item {\ptt theory_of_thm}, \bold{37}
+  \item {\ptt thin_tac}, \bold{20}
+  \item {\ptt THM} exception, 34, 35, 39, 43
+  \item {\ptt thm} ML type, 34
   \item {\ptt thms_containing}, \bold{9}
-  \item {\ptt thms_of}, \bold{57}
-  \item {\ptt tid} nonterminal, \bold{70}, 84, 91
-  \item {\ptt time_use}, \bold{3}
-  \item {\ptt time_use_thy}, \bold{53}
+  \item {\ptt thms_of}, \bold{52}
+  \item {\ptt tid} nonterminal, \bold{65}, 77, 84
+  \item {\ptt time_use}, \bold{2}
+  \item {\ptt time_use_thy}, \bold{49}
   \item timing statistics, 10
-  \item {\ptt topthm}, \bold{15}
-  \item {\ptt tpairs_of}, \bold{40}
-  \item {\ptt trace_BEST_FIRST}, \bold{32}
-  \item {\ptt trace_DEPTH_FIRST}, \bold{31}
-  \item {\ptt trace_goalno_tac}, \bold{35}
-  \item {\ptt trace_REPEAT}, \bold{29}
+  \item {\ptt topthm}, \bold{14}
+  \item {\ptt tpairs_of}, \bold{37}
+  \item {\ptt trace_BEST_FIRST}, \bold{29}
+  \item {\ptt trace_DEPTH_FIRST}, \bold{29}
+  \item {\ptt trace_goalno_tac}, \bold{32}
+  \item {\ptt trace_REPEAT}, \bold{27}
+  \item {\ptt trace_simp}, 95, 102--103
   \item tracing
-    \subitem of macros, 92
-    \subitem of searching tacticals, 31
-    \subitem of tactics, 26
-    \subitem of unification, 41
-  \item {\ptt transitive}, \bold{44}
-  \item translations, 94--97
-    \subitem parse, 78, 86
-    \subitem parse AST, \bold{84}, 85
-    \subitem print, 78
-    \subitem print AST, \bold{87}
-  \item {\ptt translations} section, 89
-  \item {\ptt trivial}, \bold{47}
-  \item {\ptt Trueprop} constant, 80
-  \item {\ptt TRY}, \bold{29, 30}
-  \item {\ptt TRYALL}, \bold{34}
-  \item {\ptt TVar}, \bold{64}
-  \item {\ptt tvar} nonterminal, \bold{70, 71}, 84, 91
-  \item {\ptt typ} ML type, 64
-  \item {\ptt Type}, \bold{64}
-  \item {\ptt type} nonterminal, \bold{70}
-  \item {\ptt type} type, 75
-  \item type constraints, 70, 78, 87
-  \item type constructors, \bold{64}
-  \item type identifiers, 70
-  \item type synonyms, \bold{51}
-  \item type unknowns, \bold{64}, 70
-    \subitem freezing/thawing of, 46
-  \item type variables, \bold{64}
-  \item types, \bold{64}
-    \subitem certified, \bold{64}
-    \subitem printing of, 3, 14, 64
+    \subitem of classical prover, 119
+    \subitem of macros, 84
+    \subitem of searching tacticals, 28, 29
+    \subitem of simplification, 95, 102--103
+    \subitem of tactics, 24
+    \subitem of unification, 38
+  \item {\ptt transitive}, \bold{41}
+  \item translations, 86--89
+    \subitem parse, 72, 79
+    \subitem parse AST, \bold{77}, 78
+    \subitem print, 72
+    \subitem print AST, \bold{80}
+  \item {\ptt translations} section, 82
+  \item {\ptt trivial}, \bold{44}
+  \item {\ptt Trueprop} constant, 73
+  \item {\ptt TRY}, \bold{27, 28}
+  \item {\ptt TRYALL}, \bold{32}
+  \item {\ptt TVar}, \bold{59}
+  \item {\ptt tvar} nonterminal, \bold{65, 66}, 77, 84
+  \item {\ptt typ} ML type, 58
+  \item {\ptt Type}, \bold{59}
+  \item {\ptt type} nonterminal, \bold{65}
+  \item {\ptt type} type, 69
+  \item type constraints, 65, 72, 80
+  \item type constructors, \bold{59}
+  \item type identifiers, 65
+  \item type synonyms, \bold{47}
+  \item type unknowns, \bold{59}, 65
+    \subitem freezing/thawing of, 42
+  \item type variables, \bold{59}
+  \item types, \bold{58}
+    \subitem certified, \bold{59}
+    \subitem printing of, 3, 14, 59
 
   \indexspace
 
   \item {\ptt undo}, 6, \bold{9}, 13
-  \item unknowns, \bold{61}, 70
-  \item {\ptt unlink_thy}, \bold{54}
-  \item {\ptt update}, \bold{54}
-  \item {\ptt uresult}, \bold{8}, 15, 56
-  \item {\ptt use}, \bold{3}
-  \item use_dir, 59, 60
-  \item {\ptt use_thy}, \bold{53}, 54, \bold{54}
+  \item unknowns, \bold{56}, 65
+  \item {\ptt unlink_thy}, \bold{50}
+  \item {\ptt update}, \bold{50}
+  \item {\ptt uresult}, \bold{8}, 14, 52
+  \item {\ptt use}, \bold{2}
+  \item use_dir, 54, 55
+  \item {\ptt use_thy}, \bold{49}, 50
 
   \indexspace
 
-  \item {\ptt Var}, \bold{61}, 86
-  \item {\ptt var} nonterminal, \bold{70, 71}, 84, 91
-  \item {\ptt Variable}, 83
+  \item {\ptt Var}, \bold{56}, 79
+  \item {\ptt var} nonterminal, \bold{65, 66}, 77, 84
+  \item {\ptt Variable}, 76
   \item variables
-    \subitem bound, \bold{61}
-    \subitem free, \bold{61}
-  \item {\ptt variant_abs}, \bold{62}, 97
-  \item {\ptt varifyT}, \bold{46}
+    \subitem bound, \bold{56}
+    \subitem free, \bold{56}
+  \item {\ptt variant_abs}, \bold{57}, 89
+  \item {\ptt varifyT}, \bold{42}
 
   \indexspace
 
   \item {\ptt xlisten} shell script, 5
-  \item {\ptt xnum} nonterminal, \bold{70}, 84, 91
-  \item {\ptt xstr} nonterminal, \bold{70}, 85, 91
+  \item {\ptt xnum} nonterminal, \bold{65}, 77, 84
+  \item {\ptt xstr} nonterminal, \bold{65}, 77, 84
 
   \indexspace
 
-  \item {\ptt zero_var_indexes}, \bold{40}
+  \item {\ptt zero_var_indexes}, \bold{36}
 
 \end{theindex}
diff -r a2de0be6e14d -r d4bed82315ab doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Wed Apr 30 13:40:40 1997 +0200
+++ b/doc-src/Ref/simplifier.tex	Wed Apr 30 16:33:43 1997 +0200
@@ -83,8 +83,9 @@
 \S\ref{sec:reordering-asms} for ways around this problem.
 \end{warn}
 
-Using the simplifier effectively may take a bit of experimentation.  The
-tactics can be traced with the ML command \verb$trace_simp := true$.
+Using the simplifier effectively may take a bit of experimentation.  
+\index{tracing!of simplification|)}\ttindex{trace_simp}
+The tactics can be traced with the ML command \verb$trace_simp := true$.
 
 There is not just one global current simpset, but one associated with each
 theory as well. How are these simpset built up?
@@ -514,6 +515,7 @@
 \end{ttbox}
 
 \subsection{An example of tracing}
+\index{tracing!of simplification|(}\ttindex{trace_simp|(}
 Let us prove a similar result involving more complex terms.  The two
 equations together can be used to prove that addition is commutative.
 \begin{ttbox}
@@ -570,6 +572,7 @@
 {\out m + Suc(n) = Suc(m + n)}
 {\out No subgoals!}
 \end{ttbox}
+\index{tracing!of simplification|)}\ttindex{trace_simp|)}
 
 \subsection{Free variables and simplification}
 Here is a conjecture to be proved for an arbitrary function~$f$ satisfying