--- 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}