diff -r 53c6ea1e6d94 -r defb086883a9 doc-src/Ref/ref.ind
--- a/doc-src/Ref/ref.ind	Fri Sep 25 14:49:12 1998 +0200
+++ b/doc-src/Ref/ref.ind	Fri Sep 25 14:54:49 1998 +0200
@@ -3,6 +3,7 @@
   \item {\tt !!} symbol, 70
   \item {\tt\$}, \bold{61}, 87
   \item {\tt\%} symbol, 70
+  \item * SplitterFun, 127
   \item {\tt ::} symbol, 70, 71
   \item {\tt ==} symbol, 70
   \item {\tt ==>} symbol, 70
@@ -26,37 +27,38 @@
   \item {\tt abstract_rule}, \bold{47}
   \item {\tt aconv}, \bold{62}
   \item {\tt addaltern}, \bold{136}
-  \item {\tt addbefore}, \bold{135}
+  \item {\tt addbefore}, \bold{136}
   \item {\tt Addcongs}, \bold{106}
   \item {\tt addcongs}, \bold{110}, 126, 127
-  \item {\tt AddDs}, \bold{140}
+  \item {\tt AddDs}, \bold{141}
   \item {\tt addDs}, \bold{134}
   \item {\tt addeqcongs}, \bold{110}, 126
-  \item {\tt AddEs}, \bold{140}
+  \item {\tt AddEs}, \bold{141}
   \item {\tt addEs}, \bold{134}
-  \item {\tt AddIs}, \bold{140}
+  \item {\tt AddIs}, \bold{141}
   \item {\tt addIs}, \bold{134}
   \item {\tt addloop}, \bold{113}
-  \item {\tt addSaltern}, \bold{135}
-  \item {\tt addSbefore}, \bold{135}
-  \item {\tt AddSDs}, \bold{140}
+  \item {\tt addSaltern}, \bold{136}
+  \item {\tt addSbefore}, \bold{136}
+  \item {\tt AddSDs}, \bold{141}
   \item {\tt addSDs}, \bold{134}
-  \item {\tt AddSEs}, \bold{140}
+  \item {\tt AddSEs}, \bold{141}
   \item {\tt addSEs}, \bold{134}
   \item {\tt Addsimprocs}, \bold{106}
   \item {\tt addsimprocs}, \bold{109}
   \item {\tt Addsimps}, \bold{106}
   \item {\tt addsimps}, \bold{109}, 127
-  \item {\tt AddSIs}, \bold{140}
+  \item {\tt AddSIs}, \bold{141}
   \item {\tt addSIs}, \bold{134}
   \item {\tt addSolver}, \bold{112}
-  \item {\tt addsplits}, \bold{113}, 126, 128
+  \item {\tt Addsplits}, \bold{106}
+  \item {\tt addsplits}, \bold{113}, 114
   \item {\tt addss}, \bold{136}, 137
   \item {\tt addSSolver}, \bold{112}
-  \item {\tt addSWrapper}, \bold{135}
-  \item {\tt addWrapper}, \bold{135}
+  \item {\tt addSWrapper}, \bold{136}
+  \item {\tt addWrapper}, \bold{136}
   \item {\tt all_tac}, \bold{33}
-  \item {\tt ALLGOALS}, \bold{37}, 117, 121
+  \item {\tt ALLGOALS}, \bold{37}, 118, 121
   \item ambiguity
     \subitem of parsed expressions, 80
   \item {\tt ancestors_of}, \bold{60}
@@ -71,25 +73,25 @@
   \item arities
     \subitem context conditions, 56
   \item {\tt Asm_full_simp_tac}, \bold{105}
-  \item {\tt asm_full_simp_tac}, 25, \bold{113}, 118
-  \item {\tt asm_full_simplify}, 114
+  \item {\tt asm_full_simp_tac}, 25, \bold{114}, 119
+  \item {\tt asm_full_simplify}, 115
   \item {\tt asm_rl} theorem, 24
   \item {\tt Asm_simp_tac}, \bold{104}, 116
-  \item {\tt asm_simp_tac}, \bold{113}, 126
-  \item {\tt asm_simplify}, 114
-  \item associative-commutative operators, 119
+  \item {\tt asm_simp_tac}, \bold{114}, 127
+  \item {\tt asm_simplify}, 115
+  \item associative-commutative operators, 120
   \item {\tt assume}, \bold{46}
   \item {\tt assume_ax}, 9, \bold{11}
   \item {\tt assume_tac}, \bold{20}, 133
   \item {\tt assumption}, \bold{49}
   \item assumptions
-    \subitem contradictory, 140
+    \subitem contradictory, 141
     \subitem deleting, 25
     \subitem in simplification, 104, 112
     \subitem inserting, 22
     \subitem negated, 131
     \subitem of main goal, 8, 9, 11, 16, 17
-    \subitem reordering, 118
+    \subitem reordering, 119
     \subitem rotating, 25
     \subitem substitution in, 101
     \subitem tactics for, 20
@@ -97,7 +99,7 @@
     \subitem made from parse trees, 85
     \subitem made from terms, 87
   \item {\tt atac}, \bold{22}
-  \item {\tt Auto_tac}, \bold{140}
+  \item {\tt Auto_tac}, \bold{141}
   \item {\tt auto_tac} $(cs,ss)$, \bold{138}
   \item {\tt axclass} section, 55
   \item axiomatic type class, 55
@@ -115,19 +117,19 @@
   \item {\tt be}, \bold{13}
   \item {\tt bes}, \bold{13}
   \item {\tt BEST_FIRST}, \bold{34}, 35
-  \item {\tt Best_tac}, \bold{140}
-  \item {\tt best_tac}, \bold{138}
+  \item {\tt Best_tac}, \bold{141}
+  \item {\tt best_tac}, \bold{139}
   \item {\tt beta_conversion}, \bold{47}
   \item {\tt bicompose}, \bold{50}
   \item {\tt bimatch_tac}, \bold{26}
   \item {\tt bind_thm}, \bold{10}, 11, 40
   \item binders, \bold{79}
   \item {\tt biresolution}, \bold{49}
-  \item {\tt biresolve_tac}, \bold{26}, 141
-  \item {\tt Blast.depth_tac}, \bold{137}
-  \item {\tt Blast.trace}, \bold{137}
-  \item {\tt Blast_tac}, \bold{140}
-  \item {\tt blast_tac}, \bold{137}
+  \item {\tt biresolve_tac}, \bold{26}, 142
+  \item {\tt Blast.depth_tac}, \bold{138}
+  \item {\tt Blast.trace}, \bold{138}
+  \item {\tt Blast_tac}, \bold{141}
+  \item {\tt blast_tac}, \bold{138}
   \item {\tt Bound}, \bold{61}, 85, 87, 88
   \item {\tt bound_hyp_subst_tac}, \bold{101}
   \item {\tt br}, \bold{13}
@@ -145,20 +147,22 @@
   \item {\tt CHANGED}, \bold{33}
   \item {\tt chop}, \bold{11}, 16
   \item {\tt choplev}, \bold{12}
-  \item {\tt Clarify_step_tac}, \bold{140}
-  \item {\tt clarify_step_tac}, \bold{136}
-  \item {\tt Clarify_tac}, \bold{140}
-  \item {\tt clarify_tac}, \bold{136}
+  \item {\tt Clarify_step_tac}, \bold{141}
+  \item {\tt clarify_step_tac}, \bold{137}
+  \item {\tt Clarify_tac}, \bold{141}
+  \item {\tt clarify_tac}, \bold{137}
+  \item {\tt clarsimp_tac}, \bold{137}
   \item claset
     \subitem current, 140
-  \item {\tt claset} ML type, 133
+  \item {\tt claset} ML type, 134
+  \item {\tt ClasimpFun}, 143
   \item classes
     \subitem context conditions, 56
-  \item classical reasoner, 129--142
-    \subitem setting up, 141
-    \subitem tactics, 136
+  \item classical reasoner, 129--143
+    \subitem setting up, 142
+    \subitem tactics, 137
   \item classical sets, 133
-  \item {\tt ClassicalFun}, 141
+  \item {\tt ClassicalFun}, 142
   \item {\tt combination}, \bold{47}
   \item {\tt commit}, \bold{2}
   \item {\tt COMP}, \bold{49}
@@ -173,7 +177,7 @@
     \subitem for translations, 74
     \subitem syntactic, 89
   \item {\tt context}, 104
-  \item {\tt contr_tac}, \bold{140}
+  \item {\tt contr_tac}, \bold{141}
   \item {\tt could_unify}, \bold{28}
   \item {\tt cprems_of}, \bold{43}
   \item {\tt cprop_of}, \bold{42}
@@ -192,7 +196,7 @@
   \indexspace
 
   \item {\tt datatype}, 106
-  \item {\tt Deepen_tac}, \bold{140}
+  \item {\tt Deepen_tac}, \bold{141}
   \item {\tt deepen_tac}, \bold{139}
   \item {\tt defer_tac}, \bold{23}
   \item definitions, \see{rewriting, meta-level}{1}, 23, \bold{56}
@@ -202,12 +206,14 @@
   \item {\tt deleqcongs}, \bold{110}
   \item {\tt delete_tmpfiles}, \bold{57}
   \item delimiters, \bold{71}, 74, 75, 77
+  \item {\tt delloop}, \bold{113}
   \item {\tt delrules}, \bold{134}
   \item {\tt Delsimprocs}, \bold{106}
   \item {\tt delsimprocs}, \bold{109}
   \item {\tt Delsimps}, \bold{106}
   \item {\tt delsimps}, \bold{109}
-  \item {\tt delSWrapper}, \bold{135}
+  \item {\tt Delsplits}, \bold{106}
+  \item {\tt delSWrapper}, \bold{136}
   \item {\tt delWrapper}, \bold{136}
   \item {\tt dependent_tr'}, 95, \bold{97}
   \item {\tt DEPTH_FIRST}, \bold{34}
@@ -241,11 +247,11 @@
   \item {\tt ematch_tac}, \bold{20}
   \item {\tt empty} constant, 93
   \item {\tt empty_cs}, \bold{134}
-  \item {\tt empty_ss}, \bold{107}
+  \item {\tt empty_ss}, \bold{108}
   \item {\tt eq_assume_tac}, \bold{20}, 133
   \item {\tt eq_assumption}, \bold{49}
   \item {\tt eq_mp_tac}, \bold{141}
-  \item {\tt eq_reflection} theorem, \bold{103}, 123
+  \item {\tt eq_reflection} theorem, \bold{103}, 124
   \item {\tt eq_thm}, \bold{35}
   \item {\tt eq_thy}, \bold{59}
   \item {\tt equal_elim}, \bold{46}
@@ -266,7 +272,7 @@
     \subitem of logic definitions, 81
     \subitem of macros, 93, 94
     \subitem of mixfix declarations, 76
-    \subitem of simplification, 115
+    \subitem of simplification, 116
     \subitem of translations, 97
   \item exceptions
     \subitem printing of, 5
@@ -276,8 +282,8 @@
   \indexspace
 
   \item {\tt fa}, \bold{14}
-  \item {\tt Fast_tac}, \bold{140}
-  \item {\tt fast_tac}, \bold{138}
+  \item {\tt Fast_tac}, \bold{141}
+  \item {\tt fast_tac}, \bold{139}
   \item {\tt fd}, \bold{14}
   \item {\tt fds}, \bold{14}
   \item {\tt fe}, \bold{14}
@@ -298,8 +304,8 @@
   \item flex-flex constraints, 25, 42, 50
   \item {\tt flexflex_rule}, \bold{50}
   \item {\tt flexflex_tac}, \bold{25}
-  \item {\tt FOL_basic_ss}, \bold{126}
-  \item {\tt FOL_ss}, \bold{126}
+  \item {\tt FOL_basic_ss}, \bold{127}
+  \item {\tt FOL_ss}, \bold{127}
   \item {\tt fold_goals_tac}, \bold{23}
   \item {\tt fold_tac}, \bold{23}
   \item {\tt forall_elim}, \bold{48}
@@ -310,7 +316,7 @@
   \item {\tt forall_intr_frees}, \bold{48}
   \item {\tt forall_intr_list}, \bold{48}
   \item {\tt force_strip_shyps}, \bold{43}
-  \item {\tt Force_tac}, \bold{140}
+  \item {\tt Force_tac}, \bold{141}
   \item {\tt force_tac}, \bold{138}
   \item {\tt forw_inst_tac}, \bold{21}
   \item forward proof, 20, 40
@@ -320,8 +326,8 @@
   \item {\tt freezeT}, \bold{48}
   \item {\tt frs}, \bold{14}
   \item {\tt Full_simp_tac}, \bold{104}
-  \item {\tt full_simp_tac}, \bold{113}
-  \item {\tt full_simplify}, 114
+  \item {\tt full_simp_tac}, \bold{114}
+  \item {\tt full_simplify}, 115
   \item {\textit {fun}} type, 64
   \item function applications, \bold{61}
 
@@ -345,8 +351,8 @@
   \item higher-order pattern, \bold{109}
   \item {\tt HOL_basic_ss}, \bold{108}
   \item {\tt hyp_subst_tac}, \bold{101}
-  \item {\tt hyp_subst_tacs}, \bold{142}
-  \item {\tt HypsubstFun}, 102, 142
+  \item {\tt hyp_subst_tacs}, \bold{143}
+  \item {\tt HypsubstFun}, 102, 143
 
   \indexspace
 
@@ -355,8 +361,8 @@
   \item {\tt idt} nonterminal, 91
   \item {\tt idts} nonterminal, \bold{71}, 79
   \item {\tt IF_UNSOLVED}, \bold{35}
-  \item {\tt iff_reflection} theorem, 123
-  \item {\tt IFOL_ss}, \bold{126}
+  \item {\tt iff_reflection} theorem, 124
+  \item {\tt IFOL_ss}, \bold{127}
   \item {\tt imp_intr} theorem, \bold{103}
   \item {\tt implies_elim}, \bold{46}
   \item {\tt implies_elim_list}, \bold{46}
@@ -367,7 +373,7 @@
   \item {\tt indexname} ML type, 61, 72
   \item infixes, \bold{78}
   \item {\tt insert} constant, 93
-  \item {\tt inst_step_tac}, \bold{139}
+  \item {\tt inst_step_tac}, \bold{140}
   \item {\tt instance} section, 55
   \item {\tt instantiate}, \bold{48}
   \item {\tt instantiate'}, \bold{41}, 48
@@ -379,7 +385,7 @@
 
   \indexspace
 
-  \item {\tt joinrules}, \bold{141}
+  \item {\tt joinrules}, \bold{142}
 
   \indexspace
 
@@ -404,7 +410,7 @@
   \indexspace
 
   \item macros, 89--95
-  \item {\tt make_elim}, \bold{42}, 134
+  \item {\tt make_elim}, \bold{42}, 135
   \item {\tt Match} exception, 96
   \item {\tt match_tac}, \bold{20}, 133
   \item {\tt max_pri}, 69, \bold{75}
@@ -416,16 +422,16 @@
   \item meta-implication, 45, 46
   \item meta-quantifiers, 45, 47
   \item meta-rewriting, 8, 14, 15, \bold{23}, 
-		\seealso{tactics, theorems}{143}
+		\seealso{tactics, theorems}{144}
     \subitem in theorems, 41
   \item meta-rules, \see{meta-rules}{1}, 44--50
   \item {\tt METAHYPS}, 18, \bold{36}
   \item mixfix declarations, 54, 74--79
-  \item {\tt mk_case_split_tac}, \bold{127}
+  \item {\tt mk_atomize}, \bold{126}
   \item {\tt mk_simproc}, \bold{122}
   \item {\tt ML} section, 56, 96, 98
   \item model checkers, 80
-  \item {\tt mp} theorem, \bold{141}
+  \item {\tt mp} theorem, \bold{142}
   \item {\tt mp_tac}, \bold{141}
   \item {\tt MRL}, \bold{40}
   \item {\tt MRS}, \bold{40}
@@ -574,7 +580,7 @@
   \item {\tt result}, \bold{9}, 11, 17
   \item {\tt rev_mp} theorem, \bold{103}
   \item rewrite rules, 108--109
-    \subitem permutative, 119--121
+    \subitem permutative, 119--122
   \item {\tt rewrite_goals_rule}, \bold{41}
   \item {\tt rewrite_goals_tac}, \bold{23}, 41
   \item {\tt rewrite_rule}, \bold{41}
@@ -599,10 +605,10 @@
   \indexspace
 
   \item {\tt safe_asm_full_simp_tac}, \bold{114}
-  \item {\tt Safe_step_tac}, \bold{140}
-  \item {\tt safe_step_tac}, 135, \bold{139}
-  \item {\tt Safe_tac}, \bold{140}
-  \item {\tt safe_tac}, \bold{139}
+  \item {\tt Safe_step_tac}, \bold{141}
+  \item {\tt safe_step_tac}, 135, \bold{140}
+  \item {\tt Safe_tac}, \bold{141}
+  \item {\tt safe_tac}, \bold{140}
   \item {\tt save_proof}, \bold{17}
   \item saving your work, \bold{1}
   \item search, 31
@@ -614,7 +620,7 @@
   \item sessions, 1--6
   \item {\tt set}, 3
   \item {\tt setloop}, \bold{113}
-  \item {\tt setmksimps}, 109, \bold{124}, 127
+  \item {\tt setmksimps}, 109, \bold{125}, 127
   \item {\tt setSolver}, \bold{112}, 127
   \item {\tt setSSolver}, \bold{112}, 127
   \item {\tt setsubgoaler}, \bold{111}, 127
@@ -640,21 +646,22 @@
   \item {\tt sign_of_thm}, \bold{43}
   \item signatures, \bold{53}, 61, 63, 65
   \item {\tt Simp_tac}, \bold{104}
-  \item {\tt simp_tac}, \bold{113}
+  \item {\tt simp_tac}, \bold{114}
   \item simplification, 104--128
-    \subitem conversions, 114
-    \subitem forward rules, 114
+    \subitem conversions, 115
+    \subitem forward rules, 115
     \subitem from classical reasoner, 136
     \subitem setting up, 123
+    \subitem setting up the splitter, 127
     \subitem setting up the theory, 128
-    \subitem tactics, 113
+    \subitem tactics, 114
   \item simplification sets, 107
-  \item {\tt Simplifier.asm_full_rewrite}, 114
-  \item {\tt Simplifier.asm_rewrite}, 114
-  \item {\tt Simplifier.full_rewrite}, 114
-  \item {\tt Simplifier.rewrite}, 114
+  \item {\tt Simplifier.asm_full_rewrite}, 115
+  \item {\tt Simplifier.asm_rewrite}, 115
+  \item {\tt Simplifier.full_rewrite}, 115
+  \item {\tt Simplifier.rewrite}, 115
   \item {\tt Simplifier.setup}, \bold{128}
-  \item {\tt simplify}, 114
+  \item {\tt simplify}, 115
   \item {\tt SIMPSET}, \bold{114}
   \item simpset
     \subitem current, 104, 108
@@ -665,9 +672,9 @@
   \item {\tt simpset_ref_of}, \bold{108}
   \item {\tt size_of_thm}, 34, \bold{35}, 142
   \item {\tt sizef}, \bold{142}
-  \item {\tt slow_best_tac}, \bold{138}
-  \item {\tt slow_step_tac}, 135, \bold{139}
-  \item {\tt slow_tac}, \bold{138}
+  \item {\tt slow_best_tac}, \bold{139}
+  \item {\tt slow_step_tac}, 135, \bold{140}
+  \item {\tt slow_tac}, \bold{139}
   \item {\tt Some}, \bold{29}
   \item {\tt SOMEGOAL}, \bold{37}
   \item {\tt sort} nonterminal, \bold{71}
@@ -675,14 +682,13 @@
   \item sort hypotheses, 43
   \item sorts
     \subitem printing of, 4
-  \item {\tt split_tac}, \bold{127}
   \item {\tt ssubst} theorem, \bold{100}
   \item {\tt stac}, \bold{101}
   \item stamps, \bold{53}, 61
   \item {\tt standard}, \bold{42}
   \item starting up, \bold{1}
-  \item {\tt Step_tac}, \bold{140}
-  \item {\tt step_tac}, 135, \bold{139}
+  \item {\tt Step_tac}, \bold{141}
+  \item {\tt step_tac}, 135, \bold{140}
   \item {\tt store_thm}, \bold{10}
   \item {\tt string_of_cterm}, \bold{63}
   \item {\tt string_of_ctyp}, \bold{65}
@@ -699,7 +705,7 @@
   \item {\tt subthy}, \bold{59}
   \item {\tt swap} theorem, \bold{142}
   \item {\tt swap_res_tac}, \bold{141}
-  \item {\tt swapify}, \bold{141}
+  \item {\tt swapify}, \bold{142}
   \item {\tt sym} theorem, 101, \bold{103}
   \item {\tt symmetric}, \bold{47}
   \item {\tt syn_of}, \bold{73}
@@ -739,16 +745,16 @@
     \subitem debugging, 17
     \subitem filtering results of, 33
     \subitem for composition, 26
-    \subitem for contradiction, 140
+    \subitem for contradiction, 141
     \subitem for inserting facts, 22
-    \subitem for Modus Ponens, 140
+    \subitem for Modus Ponens, 141
     \subitem instantiation, 21
     \subitem matching, 20
     \subitem meta-rewriting, 22, \bold{23}
     \subitem primitives for coding, 28
     \subitem resolution, \bold{19}, 22, 26, 27
     \subitem restricting to a subgoal, 36
-    \subitem simplification, 113
+    \subitem simplification, 114
     \subitem substitution, 100--103
     \subitem tracing, 29
   \item {\tt TERM}, 63
@@ -811,12 +817,12 @@
   \item {\tt trace_DEPTH_FIRST}, \bold{34}
   \item {\tt trace_goalno_tac}, \bold{37}
   \item {\tt trace_REPEAT}, \bold{32}
-  \item {\tt trace_simp}, \bold{105}, 116
+  \item {\tt trace_simp}, \bold{105}, 117
   \item tracing
-    \subitem of classical prover, 137
+    \subitem of classical prover, 138
     \subitem of macros, 93
     \subitem of searching tacticals, 34
-    \subitem of simplification, 106, 116--117
+    \subitem of simplification, 106, 117--118
     \subitem of tactics, 29
     \subitem of unification, 44
   \item {\tt transfer}, \bold{59}