1.1 --- a/doc-src/Ref/ref.ind	Mon Aug 24 19:12:13 1998 +0200
     1.2 +++ b/doc-src/Ref/ref.ind	Mon Aug 24 19:13:00 1998 +0200
     1.3 @@ -25,38 +25,38 @@
     1.4    \item {\tt abstract_over}, \bold{61}
     1.5    \item {\tt abstract_rule}, \bold{45}
     1.6    \item {\tt aconv}, \bold{61}
     1.7 -  \item {\tt addaltern}, \bold{134}
     1.8 -  \item {\tt addbefore}, \bold{133}
     1.9 +  \item {\tt addaltern}, \bold{135}
    1.10 +  \item {\tt addbefore}, \bold{134}
    1.11    \item {\tt Addcongs}, \bold{105}
    1.12 -  \item {\tt addcongs}, \bold{109}, 124, 125
    1.13 -  \item {\tt AddDs}, \bold{138}
    1.14 -  \item {\tt addDs}, \bold{132}
    1.15 -  \item {\tt addeqcongs}, \bold{109}, 124
    1.16 -  \item {\tt AddEs}, \bold{138}
    1.17 -  \item {\tt addEs}, \bold{132}
    1.18 -  \item {\tt AddIs}, \bold{138}
    1.19 -  \item {\tt addIs}, \bold{132}
    1.20 +  \item {\tt addcongs}, \bold{109}, 125, 126
    1.21 +  \item {\tt AddDs}, \bold{139}
    1.22 +  \item {\tt addDs}, \bold{133}
    1.23 +  \item {\tt addeqcongs}, \bold{109}, 125
    1.24 +  \item {\tt AddEs}, \bold{139}
    1.25 +  \item {\tt addEs}, \bold{133}
    1.26 +  \item {\tt AddIs}, \bold{139}
    1.27 +  \item {\tt addIs}, \bold{133}
    1.28    \item {\tt addloop}, \bold{112}
    1.29 -  \item {\tt addSaltern}, \bold{133}
    1.30 -  \item {\tt addSbefore}, \bold{133}
    1.31 -  \item {\tt AddSDs}, \bold{138}
    1.32 -  \item {\tt addSDs}, \bold{132}
    1.33 -  \item {\tt AddSEs}, \bold{138}
    1.34 -  \item {\tt addSEs}, \bold{132}
    1.35 +  \item {\tt addSaltern}, \bold{134}
    1.36 +  \item {\tt addSbefore}, \bold{134}
    1.37 +  \item {\tt AddSDs}, \bold{139}
    1.38 +  \item {\tt addSDs}, \bold{133}
    1.39 +  \item {\tt AddSEs}, \bold{139}
    1.40 +  \item {\tt addSEs}, \bold{133}
    1.41    \item {\tt Addsimprocs}, \bold{105}
    1.42    \item {\tt addsimprocs}, \bold{108}
    1.43    \item {\tt Addsimps}, \bold{105}
    1.44 -  \item {\tt addsimps}, \bold{108}, 125
    1.45 -  \item {\tt AddSIs}, \bold{138}
    1.46 -  \item {\tt addSIs}, \bold{132}
    1.47 +  \item {\tt addsimps}, \bold{108}, 126
    1.48 +  \item {\tt AddSIs}, \bold{139}
    1.49 +  \item {\tt addSIs}, \bold{133}
    1.50    \item {\tt addSolver}, \bold{111}
    1.51 -  \item {\tt addsplits}, \bold{112}, 124, 126
    1.52 -  \item {\tt addss}, \bold{134}, 135
    1.53 +  \item {\tt addsplits}, \bold{112}, 125, 127
    1.54 +  \item {\tt addss}, \bold{135}, 136
    1.55    \item {\tt addSSolver}, \bold{111}
    1.56 -  \item {\tt addSWrapper}, \bold{133}
    1.57 -  \item {\tt addWrapper}, \bold{133}
    1.58 +  \item {\tt addSWrapper}, \bold{134}
    1.59 +  \item {\tt addWrapper}, \bold{134}
    1.60    \item {\tt all_tac}, \bold{31}
    1.61 -  \item {\tt ALLGOALS}, \bold{35}, 116, 119
    1.62 +  \item {\tt ALLGOALS}, \bold{35}, 116, 120
    1.63    \item ambiguity
    1.64      \subitem of parsed expressions, 79
    1.65    \item {\tt ancestors_of}, \bold{59}
    1.66 @@ -67,27 +67,27 @@
    1.67    \item {\tt aprop} nonterminal, \bold{70}
    1.68    \item {\tt ares_tac}, \bold{20}
    1.69    \item {\tt args} nonterminal, 93
    1.70 -  \item {\tt Arith} theory, 118
    1.71 +  \item {\tt Arith} theory, 119
    1.72    \item arities
    1.73      \subitem context conditions, 54
    1.74    \item {\tt Asm_full_simp_tac}, \bold{104}
    1.75    \item {\tt asm_full_simp_tac}, 23, \bold{112}, 117
    1.76    \item {\tt asm_full_simplify}, 113
    1.77    \item {\tt asm_rl} theorem, 22
    1.78 -  \item {\tt Asm_simp_tac}, \bold{103}, 114
    1.79 +  \item {\tt Asm_simp_tac}, \bold{103}, 115
    1.80    \item {\tt asm_simp_tac}, \bold{112}, 125
    1.81    \item {\tt asm_simplify}, 113
    1.82    \item associative-commutative operators, 118
    1.83    \item {\tt assume}, \bold{44}
    1.84 -  \item {\tt assume_ax}, 9, \bold{57}
    1.85 -  \item {\tt assume_tac}, \bold{18}, 131
    1.86 +  \item {\tt assume_ax}, 9, \bold{58}
    1.87 +  \item {\tt assume_tac}, \bold{18}, 132
    1.88    \item {\tt assumption}, \bold{47}
    1.89    \item assumptions
    1.90 -    \subitem contradictory, 138
    1.91 +    \subitem contradictory, 139
    1.92      \subitem deleting, 23
    1.93      \subitem in simplification, 103, 111
    1.94      \subitem inserting, 20
    1.95 -    \subitem negated, 129
    1.96 +    \subitem negated, 130
    1.97      \subitem of main goal, 8--10, 15
    1.98      \subitem reordering, 117
    1.99      \subitem rotating, 23
   1.100 @@ -97,8 +97,8 @@
   1.101      \subitem made from parse trees, 84
   1.102      \subitem made from terms, 86
   1.103    \item {\tt atac}, \bold{20}
   1.104 -  \item {\tt Auto_tac}, \bold{138}
   1.105 -  \item {\tt auto_tac} $(cs,ss)$, \bold{136}
   1.106 +  \item {\tt Auto_tac}, \bold{139}
   1.107 +  \item {\tt auto_tac} $(cs,ss)$, \bold{137}
   1.108    \item {\tt axclass} section, 53
   1.109    \item axiomatic type class, 53
   1.110    \item axioms
   1.111 @@ -115,19 +115,19 @@
   1.112    \item {\tt be}, \bold{12}
   1.113    \item {\tt bes}, \bold{12}
   1.114    \item {\tt BEST_FIRST}, \bold{32}, 33
   1.115 -  \item {\tt Best_tac}, \bold{138}
   1.116 -  \item {\tt best_tac}, \bold{136}
   1.117 +  \item {\tt Best_tac}, \bold{139}
   1.118 +  \item {\tt best_tac}, \bold{137}
   1.119    \item {\tt beta_conversion}, \bold{45}
   1.120    \item {\tt bicompose}, \bold{48}
   1.121    \item {\tt bimatch_tac}, \bold{24}
   1.122    \item {\tt bind_thm}, \bold{9}, 10, 38
   1.123    \item binders, \bold{78}
   1.124    \item {\tt biresolution}, \bold{47}
   1.125 -  \item {\tt biresolve_tac}, \bold{24}, 139
   1.126 -  \item {\tt Blast.depth_tac}, \bold{135}
   1.127 -  \item {\tt Blast.trace}, \bold{135}
   1.128 -  \item {\tt Blast_tac}, \bold{138}
   1.129 -  \item {\tt blast_tac}, \bold{135}
   1.130 +  \item {\tt biresolve_tac}, \bold{24}, 140
   1.131 +  \item {\tt Blast.depth_tac}, \bold{136}
   1.132 +  \item {\tt Blast.trace}, \bold{136}
   1.133 +  \item {\tt Blast_tac}, \bold{139}
   1.134 +  \item {\tt blast_tac}, \bold{136}
   1.135    \item {\tt Bound}, \bold{60}, 84, 86, 87
   1.136    \item {\tt bound_hyp_subst_tac}, \bold{100}
   1.137    \item {\tt br}, \bold{12}
   1.138 @@ -145,20 +145,20 @@
   1.139    \item {\tt CHANGED}, \bold{31}
   1.140    \item {\tt chop}, \bold{10}, 14
   1.141    \item {\tt choplev}, \bold{10}
   1.142 -  \item {\tt Clarify_step_tac}, \bold{138}
   1.143 -  \item {\tt clarify_step_tac}, \bold{134}
   1.144 -  \item {\tt Clarify_tac}, \bold{138}
   1.145 -  \item {\tt clarify_tac}, \bold{134}
   1.146 +  \item {\tt Clarify_step_tac}, \bold{139}
   1.147 +  \item {\tt clarify_step_tac}, \bold{135}
   1.148 +  \item {\tt Clarify_tac}, \bold{139}
   1.149 +  \item {\tt clarify_tac}, \bold{135}
   1.150    \item claset
   1.151 -    \subitem current, 138
   1.152 -  \item {\tt claset} ML type, 131
   1.153 +    \subitem current, 139
   1.154 +  \item {\tt claset} ML type, 132
   1.155    \item classes
   1.156      \subitem context conditions, 54
   1.157 -  \item classical reasoner, 127--140
   1.158 -    \subitem setting up, 139
   1.159 -    \subitem tactics, 134
   1.160 -  \item classical sets, 131
   1.161 -  \item {\tt ClassicalFun}, 139
   1.162 +  \item classical reasoner, 128--141
   1.163 +    \subitem setting up, 140
   1.164 +    \subitem tactics, 135
   1.165 +  \item classical sets, 132
   1.166 +  \item {\tt ClassicalFun}, 140
   1.167    \item {\tt combination}, \bold{45}
   1.168    \item {\tt commit}, \bold{2}
   1.169    \item {\tt COMP}, \bold{47}
   1.170 @@ -173,7 +173,7 @@
   1.171      \subitem for translations, 73
   1.172      \subitem syntactic, 88
   1.173    \item {\tt context}, 103
   1.174 -  \item {\tt contr_tac}, \bold{138}
   1.175 +  \item {\tt contr_tac}, \bold{139}
   1.176    \item {\tt could_unify}, \bold{26}
   1.177    \item {\tt cprems_of}, \bold{41}
   1.178    \item {\tt cprop_of}, \bold{40}
   1.179 @@ -192,8 +192,8 @@
   1.180    \indexspace
   1.181  
   1.182    \item {\tt datatype}, 105
   1.183 -  \item {\tt Deepen_tac}, \bold{138}
   1.184 -  \item {\tt deepen_tac}, \bold{137}
   1.185 +  \item {\tt Deepen_tac}, \bold{139}
   1.186 +  \item {\tt deepen_tac}, \bold{138}
   1.187    \item {\tt defer_tac}, \bold{21}
   1.188    \item definitions, \see{rewriting, meta-level}{1}, 21, \bold{54}
   1.189      \subitem unfolding, 8, 9
   1.190 @@ -202,18 +202,18 @@
   1.191    \item {\tt deleqcongs}, \bold{109}
   1.192    \item {\tt delete_tmpfiles}, \bold{55}
   1.193    \item delimiters, \bold{70}, 73, 74, 76
   1.194 -  \item {\tt delrules}, \bold{132}
   1.195 +  \item {\tt delrules}, \bold{133}
   1.196    \item {\tt Delsimprocs}, \bold{105}
   1.197    \item {\tt delsimprocs}, \bold{108}
   1.198    \item {\tt Delsimps}, \bold{105}
   1.199    \item {\tt delsimps}, \bold{108}
   1.200 -  \item {\tt delSWrapper}, \bold{133}
   1.201 -  \item {\tt delWrapper}, \bold{134}
   1.202 +  \item {\tt delSWrapper}, \bold{134}
   1.203 +  \item {\tt delWrapper}, \bold{135}
   1.204    \item {\tt dependent_tr'}, 94, \bold{96}
   1.205    \item {\tt DEPTH_FIRST}, \bold{32}
   1.206    \item {\tt DEPTH_SOLVE}, \bold{32}
   1.207    \item {\tt DEPTH_SOLVE_1}, \bold{32}
   1.208 -  \item {\tt depth_tac}, \bold{137}
   1.209 +  \item {\tt depth_tac}, \bold{138}
   1.210    \item {\tt Deriv.drop}, \bold{49}
   1.211    \item {\tt Deriv.linear}, \bold{49}
   1.212    \item {\tt Deriv.size}, \bold{49}
   1.213 @@ -240,11 +240,11 @@
   1.214    \item elim-resolution, 17
   1.215    \item {\tt ematch_tac}, \bold{18}
   1.216    \item {\tt empty} constant, 92
   1.217 -  \item {\tt empty_cs}, \bold{132}
   1.218 +  \item {\tt empty_cs}, \bold{133}
   1.219    \item {\tt empty_ss}, \bold{106}
   1.220 -  \item {\tt eq_assume_tac}, \bold{18}, 131
   1.221 +  \item {\tt eq_assume_tac}, \bold{18}, 132
   1.222    \item {\tt eq_assumption}, \bold{47}
   1.223 -  \item {\tt eq_mp_tac}, \bold{139}
   1.224 +  \item {\tt eq_mp_tac}, \bold{140}
   1.225    \item {\tt eq_reflection} theorem, \bold{102}, 122
   1.226    \item {\tt eq_thm}, \bold{33}
   1.227    \item {\tt eq_thy}, \bold{58}
   1.228 @@ -276,8 +276,8 @@
   1.229    \indexspace
   1.230  
   1.231    \item {\tt fa}, \bold{12}
   1.232 -  \item {\tt Fast_tac}, \bold{138}
   1.233 -  \item {\tt fast_tac}, \bold{136}
   1.234 +  \item {\tt Fast_tac}, \bold{139}
   1.235 +  \item {\tt fast_tac}, \bold{137}
   1.236    \item {\tt fd}, \bold{12}
   1.237    \item {\tt fds}, \bold{12}
   1.238    \item {\tt fe}, \bold{12}
   1.239 @@ -310,8 +310,8 @@
   1.240    \item {\tt forall_intr_frees}, \bold{46}
   1.241    \item {\tt forall_intr_list}, \bold{46}
   1.242    \item {\tt force_strip_shyps}, \bold{41}
   1.243 -  \item {\tt Force_tac}, \bold{138}
   1.244 -  \item {\tt force_tac}, \bold{136}
   1.245 +  \item {\tt Force_tac}, \bold{139}
   1.246 +  \item {\tt force_tac}, \bold{137}
   1.247    \item {\tt forw_inst_tac}, \bold{19}
   1.248    \item forward proof, 18, 38
   1.249    \item {\tt forward_tac}, \bold{18}
   1.250 @@ -344,8 +344,8 @@
   1.251    \item higher-order pattern, \bold{108}
   1.252    \item {\tt HOL_basic_ss}, \bold{107}
   1.253    \item {\tt hyp_subst_tac}, \bold{100}
   1.254 -  \item {\tt hyp_subst_tacs}, \bold{140}
   1.255 -  \item {\tt HypsubstFun}, 101, 140
   1.256 +  \item {\tt hyp_subst_tacs}, \bold{141}
   1.257 +  \item {\tt HypsubstFun}, 101, 141
   1.258  
   1.259    \indexspace
   1.260  
   1.261 @@ -366,7 +366,7 @@
   1.262    \item {\tt indexname} ML type, 60, 71
   1.263    \item infixes, \bold{77}
   1.264    \item {\tt insert} constant, 92
   1.265 -  \item {\tt inst_step_tac}, \bold{137}
   1.266 +  \item {\tt inst_step_tac}, \bold{138}
   1.267    \item {\tt instance} section, 53
   1.268    \item {\tt instantiate}, \bold{46}
   1.269    \item {\tt instantiate'}, \bold{39}, 46
   1.270 @@ -378,7 +378,7 @@
   1.271  
   1.272    \indexspace
   1.273  
   1.274 -  \item {\tt joinrules}, \bold{139}
   1.275 +  \item {\tt joinrules}, \bold{140}
   1.276  
   1.277    \indexspace
   1.278  
   1.279 @@ -403,29 +403,29 @@
   1.280    \indexspace
   1.281  
   1.282    \item macros, 88--94
   1.283 -  \item {\tt make_elim}, \bold{40}, 132
   1.284 +  \item {\tt make_elim}, \bold{40}, 133
   1.285    \item {\tt Match} exception, 95
   1.286 -  \item {\tt match_tac}, \bold{18}, 131
   1.287 +  \item {\tt match_tac}, \bold{18}, 132
   1.288    \item {\tt max_pri}, 68, \bold{74}
   1.289    \item {\tt merge_ss}, \bold{107}
   1.290 -  \item {\tt merge_theories}, \bold{58}
   1.291 +  \item {\tt merge_theories}, \bold{59}
   1.292    \item meta-assumptions, 34, 42, 44, 47
   1.293      \subitem printing of, 4
   1.294    \item meta-equality, 43--45
   1.295    \item meta-implication, 43, 44
   1.296    \item meta-quantifiers, 43, 45
   1.297    \item meta-rewriting, 8, 13, 14, \bold{21}, 
   1.298 -		\seealso{tactics, theorems}{141}
   1.299 +		\seealso{tactics, theorems}{142}
   1.300      \subitem in theorems, 39
   1.301    \item meta-rules, \see{meta-rules}{1}, 42--48
   1.302    \item {\tt METAHYPS}, 16, \bold{34}
   1.303    \item mixfix declarations, 52, 73--78
   1.304 -  \item {\tt mk_case_split_tac}, \bold{125}
   1.305 -  \item {\tt mk_simproc}, \bold{120}
   1.306 -  \item {\tt ML} section, 53, 95, 97
   1.307 +  \item {\tt mk_case_split_tac}, \bold{126}
   1.308 +  \item {\tt mk_simproc}, \bold{121}
   1.309 +  \item {\tt ML} section, 54, 95, 97
   1.310    \item model checkers, 79
   1.311 -  \item {\tt mp} theorem, \bold{139}
   1.312 -  \item {\tt mp_tac}, \bold{139}
   1.313 +  \item {\tt mp} theorem, \bold{140}
   1.314 +  \item {\tt mp_tac}, \bold{140}
   1.315    \item {\tt MRL}, \bold{38}
   1.316    \item {\tt MRS}, \bold{38}
   1.317  
   1.318 @@ -439,7 +439,8 @@
   1.319    \item {\tt net_resolve_tac}, \bold{25}
   1.320    \item {\tt no_tac}, \bold{31}
   1.321    \item {\tt None}, \bold{27}
   1.322 -  \item {\tt not_elim} theorem, \bold{140}
   1.323 +  \item {\tt nonterminal} symbols, 52
   1.324 +  \item {\tt not_elim} theorem, \bold{141}
   1.325    \item {\tt nprems_of}, \bold{41}
   1.326    \item numerals, 70
   1.327  
   1.328 @@ -477,8 +478,7 @@
   1.329    \item {\tt prin}, 6, \bold{15}
   1.330    \item print mode, 52, 97
   1.331    \item print modes, 78--79
   1.332 -  \item {\tt print_cs}, \bold{132}
   1.333 -  \item {\tt print_data}, \bold{59}
   1.334 +  \item {\tt print_cs}, \bold{133}
   1.335    \item {\tt print_depth}, \bold{4}
   1.336    \item {\tt print_exn}, \bold{6}, 37
   1.337    \item {\tt print_goals}, \bold{38}
   1.338 @@ -531,7 +531,7 @@
   1.339  
   1.340    \indexspace
   1.341  
   1.342 -  \item {\tt qed}, \bold{9}, 10, 57
   1.343 +  \item {\tt qed}, \bold{9}, 10, 58
   1.344    \item {\tt qed_goal}, \bold{14}
   1.345    \item {\tt qed_goalw}, \bold{14}
   1.346    \item quantifiers, 78
   1.347 @@ -552,7 +552,7 @@
   1.348    \item {\tt rename_last_tac}, \bold{22}
   1.349    \item {\tt rename_params_rule}, \bold{48}
   1.350    \item {\tt rename_tac}, \bold{22}
   1.351 -  \item {\tt rep_cs}, \bold{132}
   1.352 +  \item {\tt rep_cs}, \bold{133}
   1.353    \item {\tt rep_cterm}, \bold{62}
   1.354    \item {\tt rep_ctyp}, \bold{64}
   1.355    \item {\tt rep_ss}, \bold{106}
   1.356 @@ -568,19 +568,19 @@
   1.357    \item resolution, 38, 47
   1.358      \subitem tactics, 17
   1.359      \subitem without lifting, 47
   1.360 -  \item {\tt resolve_tac}, \bold{17}, 131
   1.361 +  \item {\tt resolve_tac}, \bold{17}, 132
   1.362    \item {\tt restore_proof}, \bold{15}
   1.363 -  \item {\tt result}, \bold{9}, 16, 57
   1.364 +  \item {\tt result}, \bold{9}, 16, 58
   1.365    \item {\tt rev_mp} theorem, \bold{102}
   1.366    \item rewrite rules, 107--108
   1.367 -    \subitem permutative, 117--120
   1.368 +    \subitem permutative, 118--120
   1.369    \item {\tt rewrite_goals_rule}, \bold{39}
   1.370    \item {\tt rewrite_goals_tac}, \bold{21}, 39
   1.371    \item {\tt rewrite_rule}, \bold{39}
   1.372    \item {\tt rewrite_tac}, 9, \bold{21}
   1.373    \item rewriting
   1.374      \subitem object-level, \see{simplification}{1}
   1.375 -    \subitem ordered, 117
   1.376 +    \subitem ordered, 118
   1.377      \subitem syntactic, 88--94
   1.378    \item {\tt rewtac}, \bold{20}
   1.379    \item {\tt RL}, \bold{38}
   1.380 @@ -598,10 +598,10 @@
   1.381    \indexspace
   1.382  
   1.383    \item {\tt safe_asm_full_simp_tac}, \bold{113}
   1.384 -  \item {\tt Safe_step_tac}, \bold{138}
   1.385 -  \item {\tt safe_step_tac}, 133, \bold{137}
   1.386 -  \item {\tt Safe_tac}, \bold{138}
   1.387 -  \item {\tt safe_tac}, \bold{137}
   1.388 +  \item {\tt Safe_step_tac}, \bold{139}
   1.389 +  \item {\tt safe_step_tac}, 134, \bold{138}
   1.390 +  \item {\tt Safe_tac}, \bold{139}
   1.391 +  \item {\tt safe_tac}, \bold{138}
   1.392    \item {\tt save_proof}, \bold{15}
   1.393    \item saving your work, \bold{1}
   1.394    \item search, 29
   1.395 @@ -609,15 +609,18 @@
   1.396    \item {\tt SELECT_GOAL}, 21, \bold{34}
   1.397    \item {\tt Seq.seq} ML type, 26
   1.398    \item sequences (lazy lists), \bold{27}
   1.399 -  \item sequent calculus, 128
   1.400 +  \item sequent calculus, 129
   1.401    \item sessions, 1--6
   1.402    \item {\tt set}, 3
   1.403    \item {\tt setloop}, \bold{112}
   1.404 -  \item {\tt setmksimps}, 108, \bold{123}, 125
   1.405 -  \item {\tt setSolver}, \bold{111}, 125
   1.406 -  \item {\tt setSSolver}, \bold{111}, 125
   1.407 -  \item {\tt setsubgoaler}, \bold{110}, 125
   1.408 -  \item {\tt settermless}, \bold{117}
   1.409 +  \item {\tt setmksimps}, 108, \bold{123}, 126
   1.410 +  \item {\tt setSolver}, \bold{111}, 126
   1.411 +  \item {\tt setSSolver}, \bold{111}, 126
   1.412 +  \item {\tt setsubgoaler}, \bold{110}, 126
   1.413 +  \item {\tt settermless}, \bold{118}
   1.414 +  \item {\tt setup}
   1.415 +    \subitem simplifier, 127
   1.416 +    \subitem theory, 53
   1.417    \item shortcuts
   1.418      \subitem for \texttt{by} commands, 11
   1.419      \subitem for tactics, 20
   1.420 @@ -637,12 +640,19 @@
   1.421    \item signatures, \bold{51}, 59, 61, 62, 64
   1.422    \item {\tt Simp_tac}, \bold{103}
   1.423    \item {\tt simp_tac}, \bold{112}
   1.424 -  \item simplification, 103--126
   1.425 +  \item simplification, 103--127
   1.426 +    \subitem conversions, 113
   1.427      \subitem forward rules, 113
   1.428 -    \subitem from classical reasoner, 134
   1.429 -    \subitem setting up, 121
   1.430 +    \subitem from classical reasoner, 135
   1.431 +    \subitem setting up, 122
   1.432 +    \subitem setting up the theory, 127
   1.433      \subitem tactics, 112
   1.434    \item simplification sets, 106
   1.435 +  \item {\tt Simplifier.asm_full_rewrite}, 113
   1.436 +  \item {\tt Simplifier.asm_rewrite}, 113
   1.437 +  \item {\tt Simplifier.full_rewrite}, 113
   1.438 +  \item {\tt Simplifier.rewrite}, 113
   1.439 +  \item {\tt Simplifier.setup}, \bold{127}
   1.440    \item {\tt simplify}, 113
   1.441    \item {\tt SIMPSET}, \bold{113}
   1.442    \item simpset
   1.443 @@ -652,12 +662,11 @@
   1.444    \item {\tt simpset_of}, \bold{107}
   1.445    \item {\tt simpset_ref}, \bold{107}
   1.446    \item {\tt simpset_ref_of}, \bold{107}
   1.447 -  \item {\tt simpset_thy_data}, \bold{126}
   1.448 -  \item {\tt size_of_thm}, 32, \bold{33}, 140
   1.449 -  \item {\tt sizef}, \bold{140}
   1.450 -  \item {\tt slow_best_tac}, \bold{136}
   1.451 -  \item {\tt slow_step_tac}, 133, \bold{137}
   1.452 -  \item {\tt slow_tac}, \bold{136}
   1.453 +  \item {\tt size_of_thm}, 32, \bold{33}, 141
   1.454 +  \item {\tt sizef}, \bold{141}
   1.455 +  \item {\tt slow_best_tac}, \bold{137}
   1.456 +  \item {\tt slow_step_tac}, 134, \bold{138}
   1.457 +  \item {\tt slow_tac}, \bold{137}
   1.458    \item {\tt Some}, \bold{27}
   1.459    \item {\tt SOMEGOAL}, \bold{35}
   1.460    \item {\tt sort} nonterminal, \bold{70}
   1.461 @@ -665,14 +674,14 @@
   1.462    \item sort hypotheses, 41
   1.463    \item sorts
   1.464      \subitem printing of, 4
   1.465 -  \item {\tt split_tac}, \bold{125}
   1.466 +  \item {\tt split_tac}, \bold{126}
   1.467    \item {\tt ssubst} theorem, \bold{99}
   1.468    \item {\tt stac}, \bold{100}
   1.469    \item stamps, \bold{51}, 59
   1.470    \item {\tt standard}, \bold{40}
   1.471    \item starting up, \bold{1}
   1.472 -  \item {\tt Step_tac}, \bold{138}
   1.473 -  \item {\tt step_tac}, 133, \bold{137}
   1.474 +  \item {\tt Step_tac}, \bold{139}
   1.475 +  \item {\tt step_tac}, 134, \bold{138}
   1.476    \item {\tt store_thm}, \bold{9}
   1.477    \item {\tt string_of_cterm}, \bold{62}
   1.478    \item {\tt string_of_ctyp}, \bold{63}
   1.479 @@ -687,9 +696,9 @@
   1.480    \item substitution
   1.481      \subitem rules, 99
   1.482    \item {\tt subthy}, \bold{58}
   1.483 -  \item {\tt swap} theorem, \bold{140}
   1.484 -  \item {\tt swap_res_tac}, \bold{139}
   1.485 -  \item {\tt swapify}, \bold{139}
   1.486 +  \item {\tt swap} theorem, \bold{141}
   1.487 +  \item {\tt swap_res_tac}, \bold{140}
   1.488 +  \item {\tt swapify}, \bold{140}
   1.489    \item {\tt sym} theorem, 100, \bold{102}
   1.490    \item {\tt symmetric}, \bold{45}
   1.491    \item {\tt syn_of}, \bold{72}
   1.492 @@ -729,9 +738,9 @@
   1.493      \subitem debugging, 15
   1.494      \subitem filtering results of, 31
   1.495      \subitem for composition, 24
   1.496 -    \subitem for contradiction, 138
   1.497 +    \subitem for contradiction, 139
   1.498      \subitem for inserting facts, 20
   1.499 -    \subitem for Modus Ponens, 138
   1.500 +    \subitem for Modus Ponens, 139
   1.501      \subitem instantiation, 19
   1.502      \subitem matching, 18
   1.503      \subitem meta-rewriting, 20, \bold{21}
   1.504 @@ -771,7 +780,7 @@
   1.505      \subitem loading, 55
   1.506      \subitem parent, \bold{51}
   1.507      \subitem pseudo, \bold{56}
   1.508 -    \subitem reloading, \bold{55}
   1.509 +    \subitem reloading, \bold{56}
   1.510      \subitem removing, \bold{56}
   1.511      \subitem theorems of, 57
   1.512    \item {\tt THEORY} exception, 51, 57
   1.513 @@ -784,7 +793,6 @@
   1.514    \item {\tt thm} ML type, 37
   1.515    \item {\tt thms_containing}, \bold{10}
   1.516    \item {\tt thms_of}, \bold{57}
   1.517 -  \item {\tt thy_data}, \bold{126}
   1.518    \item {\tt tid} nonterminal, \bold{70}, 84, 91
   1.519    \item {\tt time_use}, \bold{3}
   1.520    \item {\tt time_use_thy}, \bold{55}
   1.521 @@ -802,7 +810,7 @@
   1.522    \item {\tt trace_REPEAT}, \bold{30}
   1.523    \item {\tt trace_simp}, \bold{104}, 115
   1.524    \item tracing
   1.525 -    \subitem of classical prover, 135
   1.526 +    \subitem of classical prover, 136
   1.527      \subitem of macros, 92
   1.528      \subitem of searching tacticals, 32
   1.529      \subitem of simplification, 105, 115--116
   1.530 @@ -844,7 +852,7 @@
   1.531    \item unknowns, \bold{60}, 70
   1.532    \item {\tt unlink_thy}, \bold{56}
   1.533    \item {\tt update}, \bold{56}
   1.534 -  \item {\tt uresult}, \bold{9}, 16, 57
   1.535 +  \item {\tt uresult}, \bold{9}, 16, 58
   1.536    \item {\tt use}, \bold{3}
   1.537    \item {\tt use_thy}, \bold{55}
   1.538  

     2.1 --- a/doc-src/Ref/ref.rao	Mon Aug 24 19:12:13 1998 +0200
     2.2 +++ b/doc-src/Ref/ref.rao	Mon Aug 24 19:13:00 1998 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  % This file was generated by 'rail' from 'ref.rai'
     2.5  \rail@t {lbrace}
     2.6  \rail@t {rbrace}
     2.7 -\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()) ; \par name: id | string ; \par extension : (section +) 'end' ( () | ml ) ; \par section : classes | default | types | arities | consts | syntax | trans | defs | constdefs | rules | axclass | instance | oracle | local | global ; \par classes : 'classes' ( classDecl + ) ; \par classDecl : (id (() | '<' (id + ','))) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) (() | string) nat ; \par typeDecl : typevarlist name ( () | '=' ( string | type ) ); \par typevarlist : () | tid | '(' ( tid + ',' ) ')'; \par type : simpleType | '(' type ')' | type '=>' type | '[' ( type + "," ) ']' '=>' type; \par simpleType: id | ( tid ( () | '::' id ) ) | '(' ( type + "," ) ')' id | simpleType id ; \par arities : 'arities' ((name + ',') '::' arity +) ; \par arity : ( () | '(' (sort + ',') ')' ) sort ; \par consts : 'consts' ( mixfixConstDecl + ) ; \par syntax : 'syntax' (() | mode) ( mixfixConstDecl + ); \par mode : '(' name (() | 'output') ')' ; \par mixfixConstDecl : constDecl (() | ( '(' mixfix ')' )) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par constdefs : 'constdefs' (name '::' (string | type) (() | mixfix) string +) ; \par axclass : 'axclass' classDecl (() | ( id string ) +) ; \par instance : 'instance' ( name '<' name | name '::' arity) witness ; \par witness : (() | '(' ((string | longident) + ',') ')') (() | verbatim) ; \par oracle : 'oracle' name '=' name ; \par local : 'local' ; \par global : 'global' ; \par ml : 'ML' text ; \par }
     2.8 +\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()) ; \par name : id | string ; \par extension : (section +) 'end' ( () | ml ) ; \par section : classes | default | types | arities | nonterminals | consts | syntax | trans | defs | constdefs | rules | axclass | instance | oracle | local | global | setup ; \par classes : 'classes' ( classDecl + ) ; \par classDecl : (id (() | '<' (id + ','))) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) (() | string) nat ; \par typeDecl : typevarlist name ( () | '=' ( string | type ) ); \par typevarlist : () | tid | '(' ( tid + ',' ) ')'; \par type : simpleType | '(' type ')' | type '=>' type | '[' ( type + "," ) ']' '=>' type; \par simpleType: id | ( tid ( () | '::' id ) ) | '(' ( type + "," ) ')' id | simpleType id ; \par arities : 'arities' ((name + ',') '::' arity +) ; \par arity : ( () | '(' (sort + ',') ')' ) sort ; \par nonterminals : 'nonterminals' (name+) ; \par consts : 'consts' ( mixfixConstDecl + ) ; \par syntax : 'syntax' (() | mode) ( mixfixConstDecl + ); \par mode : '(' name (() | 'output') ')' ; \par mixfixConstDecl : constDecl (() | ( '(' mixfix ')' )) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par constdefs : 'constdefs' (name '::' (string | type) (() | mixfix) string +) ; \par axclass : 'axclass' classDecl (() | ( id string ) +) ; \par instance : 'instance' ( name '<' name | name '::' arity) witness ; \par witness : (() | '(' ((string | id | longident) + ',') ')') (() | verbatim) ; \par oracle : 'oracle' name '=' name ; \par local : 'local' ; \par global : 'global' ; \par setup : 'setup' (id | longident) ; \par ml : 'ML' text ; \par }
     2.9  \rail@o {1}{
    2.10  \rail@begin{2}{theoryDef}
    2.11  \rail@nont{id}[]
    2.12 @@ -35,7 +35,7 @@
    2.13  \rail@nont{ml}[]
    2.14  \rail@endbar
    2.15  \rail@end
    2.16 -\rail@begin{15}{section}
    2.17 +\rail@begin{17}{section}
    2.18  \rail@bar
    2.19  \rail@nont{classes}[]
    2.20  \rail@nextbar{1}
    2.21 @@ -45,27 +45,31 @@
    2.22  \rail@nextbar{3}
    2.23  \rail@nont{arities}[]
    2.24  \rail@nextbar{4}
    2.25 +\rail@nont{nonterminals}[]
    2.26 +\rail@nextbar{5}
    2.27  \rail@nont{consts}[]
    2.28 -\rail@nextbar{5}
    2.29 +\rail@nextbar{6}
    2.30  \rail@nont{syntax}[]
    2.31 -\rail@nextbar{6}
    2.32 +\rail@nextbar{7}
    2.33  \rail@nont{trans}[]
    2.34 -\rail@nextbar{7}
    2.35 +\rail@nextbar{8}
    2.36  \rail@nont{defs}[]
    2.37 -\rail@nextbar{8}
    2.38 +\rail@nextbar{9}
    2.39  \rail@nont{constdefs}[]
    2.40 -\rail@nextbar{9}
    2.41 +\rail@nextbar{10}
    2.42  \rail@nont{rules}[]
    2.43 -\rail@nextbar{10}
    2.44 +\rail@nextbar{11}
    2.45  \rail@nont{axclass}[]
    2.46 -\rail@nextbar{11}
    2.47 +\rail@nextbar{12}
    2.48  \rail@nont{instance}[]
    2.49 -\rail@nextbar{12}
    2.50 +\rail@nextbar{13}
    2.51  \rail@nont{oracle}[]
    2.52 -\rail@nextbar{13}
    2.53 +\rail@nextbar{14}
    2.54  \rail@nont{local}[]
    2.55 -\rail@nextbar{14}
    2.56 +\rail@nextbar{15}
    2.57  \rail@nont{global}[]
    2.58 +\rail@nextbar{16}
    2.59 +\rail@nont{setup}[]
    2.60  \rail@endbar
    2.61  \rail@end
    2.62  \rail@begin{2}{classes}
    2.63 @@ -232,6 +236,13 @@
    2.64  \rail@endbar
    2.65  \rail@nont{sort}[]
    2.66  \rail@end
    2.67 +\rail@begin{2}{nonterminals}
    2.68 +\rail@term{nonterminals}[]
    2.69 +\rail@plus
    2.70 +\rail@nont{name}[]
    2.71 +\rail@nextplus{1}
    2.72 +\rail@endplus
    2.73 +\rail@end
    2.74  \rail@begin{2}{consts}
    2.75  \rail@term{consts}[]
    2.76  \rail@plus
    2.77 @@ -389,7 +400,7 @@
    2.78  \rail@endbar
    2.79  \rail@nont{witness}[]
    2.80  \rail@end
    2.81 -\rail@begin{4}{witness}
    2.82 +\rail@begin{5}{witness}
    2.83  \rail@bar
    2.84  \rail@nextbar{1}
    2.85  \rail@term{(}[]
    2.86 @@ -397,9 +408,11 @@
    2.87  \rail@bar
    2.88  \rail@nont{string}[]
    2.89  \rail@nextbar{2}
    2.90 +\rail@nont{id}[]
    2.91 +\rail@nextbar{3}
    2.92  \rail@nont{longident}[]
    2.93  \rail@endbar
    2.94 -\rail@nextplus{3}
    2.95 +\rail@nextplus{4}
    2.96  \rail@cterm{,}[]
    2.97  \rail@endplus
    2.98  \rail@term{)}[]
    2.99 @@ -421,6 +434,14 @@
   2.100  \rail@begin{1}{global}
   2.101  \rail@term{global}[]
   2.102  \rail@end
   2.103 +\rail@begin{2}{setup}
   2.104 +\rail@term{setup}[]
   2.105 +\rail@bar
   2.106 +\rail@nont{id}[]
   2.107 +\rail@nextbar{1}
   2.108 +\rail@nont{longident}[]
   2.109 +\rail@endbar
   2.110 +\rail@end
   2.111  \rail@begin{1}{ml}
   2.112  \rail@term{ML}[]
   2.113  \rail@nont{text}[]