Automatic update
authorpaulson
Fri Jul 04 12:36:00 1997 +0200 (1997-07-04)
changeset 3498807549666b9c
parent 3497 122e80826c95
child 3499 ce1664057431
Automatic update
doc-src/Logics/logics.ind
doc-src/Ref/ref.ind
     1.1 --- a/doc-src/Logics/logics.ind	Fri Jul 04 12:32:31 1997 +0200
     1.2 +++ b/doc-src/Logics/logics.ind	Fri Jul 04 12:36:00 1997 +0200
     1.3 @@ -3,62 +3,62 @@
     1.4    \item {\tt !} symbol, 60, 62, 69, 70
     1.5    \item {\tt[]} symbol, 81
     1.6    \item {\tt\#} symbol, 81
     1.7 -  \item {\tt\#*} symbol, 47, 124
     1.8 -  \item {\tt\#+} symbol, 47, 124
     1.9 +  \item {\tt\#*} symbol, 47, 127
    1.10 +  \item {\tt\#+} symbol, 47, 127
    1.11    \item {\tt\#-} symbol, 47
    1.12 -  \item {\tt\&} symbol, 7, 60, 101
    1.13 -  \item {\tt *} symbol, 26, 61, 78, 115
    1.14 +  \item {\tt\&} symbol, 7, 60, 104
    1.15 +  \item {\tt *} symbol, 26, 61, 78, 118
    1.16    \item {\tt *} type, 76
    1.17 -  \item {\tt +} symbol, 43, 61, 78, 115
    1.18 +  \item {\tt +} symbol, 43, 61, 78, 118
    1.19    \item {\tt +} type, 76
    1.20 -  \item {\tt -} symbol, 25, 61, 78, 124
    1.21 -  \item {\tt -->} symbol, 7, 60, 101, 115
    1.22 +  \item {\tt -} symbol, 25, 61, 78, 127
    1.23 +  \item {\tt -->} symbol, 7, 60, 104, 118
    1.24    \item {\tt ->} symbol, 26
    1.25    \item {\tt -``} symbol, 25
    1.26    \item {\tt :} symbol, 25, 68
    1.27    \item {\tt <} constant, 79
    1.28    \item {\tt <} symbol, 78
    1.29 -  \item {\tt <->} symbol, 7, 101
    1.30 +  \item {\tt <->} symbol, 7, 104
    1.31    \item {\tt <=} constant, 79
    1.32    \item {\tt <=} symbol, 25, 68
    1.33 -  \item {\tt =} symbol, 7, 60, 101, 115
    1.34 +  \item {\tt =} symbol, 7, 60, 104, 118
    1.35    \item {\tt ?} symbol, 60, 62, 69, 70
    1.36    \item {\tt ?!} symbol, 60
    1.37    \item {\tt\at} symbol, 60, 81
    1.38 -  \item {\tt `} symbol, 25, 115
    1.39 +  \item {\tt `} symbol, 25, 118
    1.40    \item {\tt ``} symbol, 25, 68
    1.41    \item \verb'{}' symbol, 68
    1.42 -  \item {\tt |} symbol, 7, 60, 101
    1.43 -  \item {\tt |-|} symbol, 124
    1.44 +  \item {\tt |} symbol, 7, 60, 104
    1.45 +  \item {\tt |-|} symbol, 127
    1.46  
    1.47    \indexspace
    1.48  
    1.49 -  \item {\tt 0} constant, 25, 78, 113
    1.50 +  \item {\tt 0} constant, 25, 78, 116
    1.51  
    1.52    \indexspace
    1.53  
    1.54 -  \item {\tt absdiff_def} theorem, 124
    1.55 -  \item {\tt add_assoc} theorem, 124
    1.56 -  \item {\tt add_commute} theorem, 124
    1.57 -  \item {\tt add_def} theorem, 47, 124
    1.58 -  \item {\tt add_inverse_diff} theorem, 124
    1.59 -  \item {\tt add_mp_tac}, \bold{122}
    1.60 -  \item {\tt add_mult_dist} theorem, 47, 124
    1.61 -  \item {\tt add_safes}, \bold{107}
    1.62 -  \item {\tt add_typing} theorem, 124
    1.63 -  \item {\tt add_unsafes}, \bold{107}
    1.64 -  \item {\tt addC0} theorem, 124
    1.65 -  \item {\tt addC_succ} theorem, 124
    1.66 -  \item {\tt ALL} symbol, 7, 26, 60, 62, 69, 70, 101
    1.67 -  \item {\tt All} constant, 7, 60, 101
    1.68 +  \item {\tt absdiff_def} theorem, 127
    1.69 +  \item {\tt add_assoc} theorem, 127
    1.70 +  \item {\tt add_commute} theorem, 127
    1.71 +  \item {\tt add_def} theorem, 47, 127
    1.72 +  \item {\tt add_inverse_diff} theorem, 127
    1.73 +  \item {\tt add_mp_tac}, \bold{125}
    1.74 +  \item {\tt add_mult_dist} theorem, 47, 127
    1.75 +  \item {\tt add_safes}, \bold{110}
    1.76 +  \item {\tt add_typing} theorem, 127
    1.77 +  \item {\tt add_unsafes}, \bold{110}
    1.78 +  \item {\tt addC0} theorem, 127
    1.79 +  \item {\tt addC_succ} theorem, 127
    1.80 +  \item {\tt ALL} symbol, 7, 26, 60, 62, 69, 70, 104
    1.81 +  \item {\tt All} constant, 7, 60, 104
    1.82    \item {\tt All_def} theorem, 64
    1.83    \item {\tt all_dupE} theorem, 5, 9, 66
    1.84    \item {\tt all_impE} theorem, 9
    1.85    \item {\tt allE} theorem, 5, 9, 66
    1.86    \item {\tt allI} theorem, 8, 66
    1.87 -  \item {\tt allL} theorem, 103, 106
    1.88 -  \item {\tt allL_thin} theorem, 104
    1.89 -  \item {\tt allR} theorem, 103
    1.90 +  \item {\tt allL} theorem, 106, 109
    1.91 +  \item {\tt allL_thin} theorem, 107
    1.92 +  \item {\tt allR} theorem, 106
    1.93    \item {\tt and_def} theorem, 42, 64
    1.94    \item {\tt app_def} theorem, 49
    1.95    \item {\tt apply_def} theorem, 31
    1.96 @@ -68,10 +68,10 @@
    1.97    \item {\tt apply_Pair} theorem, 39, 57
    1.98    \item {\tt apply_type} theorem, 39
    1.99    \item {\tt arg_cong} theorem, 65
   1.100 -  \item {\tt Arith} theory, 46, 79, 123
   1.101 +  \item {\tt Arith} theory, 46, 79, 126
   1.102    \item assumptions
   1.103      \subitem contradictory, 16
   1.104 -    \subitem in {\CTT}, 112, 122
   1.105 +    \subitem in {\CTT}, 115, 125
   1.106  
   1.107    \indexspace
   1.108  
   1.109 @@ -80,9 +80,9 @@
   1.110    \item {\tt Ball_def} theorem, 30, 71
   1.111    \item {\tt ballE} theorem, 32, 33, 72
   1.112    \item {\tt ballI} theorem, 33, 72
   1.113 -  \item {\tt basic} theorem, 103
   1.114 -  \item {\tt basic_defs}, \bold{120}
   1.115 -  \item {\tt best_tac}, \bold{108}
   1.116 +  \item {\tt basic} theorem, 106
   1.117 +  \item {\tt basic_defs}, \bold{123}
   1.118 +  \item {\tt best_tac}, \bold{111}
   1.119    \item {\tt beta} theorem, 39, 40
   1.120    \item {\tt Bex} constant, 25, 29, 68, 70
   1.121    \item {\tt bex_cong} theorem, 32, 33
   1.122 @@ -98,7 +98,7 @@
   1.123    \item {\tt blast_tac}, 18, 20, 21
   1.124    \item {\tt bnd_mono_def} theorem, 44
   1.125    \item {\tt Bool} theory, 40
   1.126 -  \item {\tt bool} type, 61
   1.127 +  \item {\textit {bool}} type, 61
   1.128    \item {\tt bool_0I} theorem, 42
   1.129    \item {\tt bool_1I} theorem, 42
   1.130    \item {\tt bool_def} theorem, 42
   1.131 @@ -118,23 +118,23 @@
   1.132    \item {\tt ccontr} theorem, 66
   1.133    \item {\tt classical} theorem, 66
   1.134    \item {\tt coinduct} theorem, 44
   1.135 -  \item {\tt coinductive}, 92--95
   1.136 +  \item {\tt coinductive}, 95--98
   1.137    \item {\tt Collect} constant, 25, 26, 29, 68, 70
   1.138    \item {\tt Collect_def} theorem, 30
   1.139    \item {\tt Collect_mem_eq} theorem, 70, 71
   1.140    \item {\tt Collect_subset} theorem, 36
   1.141 -  \item {\tt CollectD} theorem, 72, 98
   1.142 +  \item {\tt CollectD} theorem, 72, 101
   1.143    \item {\tt CollectD1} theorem, 32, 34
   1.144    \item {\tt CollectD2} theorem, 32, 34
   1.145    \item {\tt CollectE} theorem, 32, 34, 72
   1.146 -  \item {\tt CollectI} theorem, 34, 72, 98
   1.147 +  \item {\tt CollectI} theorem, 34, 72, 101
   1.148    \item {\tt comp_assoc} theorem, 45
   1.149    \item {\tt comp_bij} theorem, 45
   1.150    \item {\tt comp_def} theorem, 45
   1.151    \item {\tt comp_func} theorem, 45
   1.152    \item {\tt comp_func_apply} theorem, 45
   1.153    \item {\tt comp_inj} theorem, 45
   1.154 -  \item {\tt comp_rls}, \bold{120}
   1.155 +  \item {\tt comp_rls}, \bold{123}
   1.156    \item {\tt comp_surj} theorem, 45
   1.157    \item {\tt comp_type} theorem, 45
   1.158    \item {\tt Compl} constant, 68
   1.159 @@ -155,12 +155,12 @@
   1.160    \item {\tt conj_impE} theorem, 9, 10
   1.161    \item {\tt conjE} theorem, 9, 65
   1.162    \item {\tt conjI} theorem, 8, 65
   1.163 -  \item {\tt conjL} theorem, 103
   1.164 -  \item {\tt conjR} theorem, 103
   1.165 +  \item {\tt conjL} theorem, 106
   1.166 +  \item {\tt conjR} theorem, 106
   1.167    \item {\tt conjunct1} theorem, 8, 65
   1.168    \item {\tt conjunct2} theorem, 8, 65
   1.169 -  \item {\tt conL} theorem, 104
   1.170 -  \item {\tt conR} theorem, 104
   1.171 +  \item {\tt conL} theorem, 107
   1.172 +  \item {\tt conR} theorem, 107
   1.173    \item {\tt cons} constant, 25, 26
   1.174    \item {\tt cons_def} theorem, 31
   1.175    \item {\tt Cons_iff} theorem, 49
   1.176 @@ -169,37 +169,37 @@
   1.177    \item {\tt ConsI} theorem, 49
   1.178    \item {\tt consI1} theorem, 35
   1.179    \item {\tt consI2} theorem, 35
   1.180 -  \item Constructive Type Theory, 112--134
   1.181 -  \item {\tt contr} constant, 113
   1.182 +  \item Constructive Type Theory, 115--137
   1.183 +  \item {\tt contr} constant, 116
   1.184    \item {\tt converse} constant, 25, 39
   1.185    \item {\tt converse_def} theorem, 31
   1.186 -  \item {\tt could_res}, \bold{105}
   1.187 -  \item {\tt could_resolve_seq}, \bold{106}
   1.188 -  \item {\tt CTT} theory, 1, 112
   1.189 +  \item {\tt could_res}, \bold{108}
   1.190 +  \item {\tt could_resolve_seq}, \bold{109}
   1.191 +  \item {\tt CTT} theory, 1, 115
   1.192    \item {\tt Cube} theory, 1
   1.193 -  \item {\tt cut} theorem, 103
   1.194 +  \item {\tt cut} theorem, 106
   1.195    \item {\tt cut_facts_tac}, 18, 19, 56
   1.196 -  \item {\tt cutL_tac}, \bold{105}
   1.197 -  \item {\tt cutR_tac}, \bold{105}
   1.198 +  \item {\tt cutL_tac}, \bold{108}
   1.199 +  \item {\tt cutR_tac}, \bold{108}
   1.200  
   1.201    \indexspace
   1.202  
   1.203 -  \item {\tt datatype}, 85--92
   1.204 +  \item {\tt datatype}, 85--90
   1.205    \item {\tt deepen_tac}, 16
   1.206 -  \item {\tt diff_0_eq_0} theorem, 124
   1.207 +  \item {\tt diff_0_eq_0} theorem, 127
   1.208    \item {\tt Diff_cancel} theorem, 41
   1.209    \item {\tt Diff_contains} theorem, 36
   1.210    \item {\tt Diff_def} theorem, 30
   1.211 -  \item {\tt diff_def} theorem, 47, 124
   1.212 +  \item {\tt diff_def} theorem, 47, 127
   1.213    \item {\tt Diff_disjoint} theorem, 41
   1.214    \item {\tt Diff_Int} theorem, 41
   1.215    \item {\tt Diff_partition} theorem, 41
   1.216 -  \item {\tt diff_self_eq_0} theorem, 124
   1.217 +  \item {\tt diff_self_eq_0} theorem, 127
   1.218    \item {\tt Diff_subset} theorem, 36
   1.219 -  \item {\tt diff_succ_succ} theorem, 124
   1.220 -  \item {\tt diff_typing} theorem, 124
   1.221 +  \item {\tt diff_succ_succ} theorem, 127
   1.222 +  \item {\tt diff_typing} theorem, 127
   1.223    \item {\tt Diff_Un} theorem, 41
   1.224 -  \item {\tt diffC0} theorem, 124
   1.225 +  \item {\tt diffC0} theorem, 127
   1.226    \item {\tt DiffD1} theorem, 35
   1.227    \item {\tt DiffD2} theorem, 35
   1.228    \item {\tt DiffE} theorem, 35
   1.229 @@ -209,12 +209,13 @@
   1.230    \item {\tt disjE} theorem, 8, 65
   1.231    \item {\tt disjI1} theorem, 8, 65
   1.232    \item {\tt disjI2} theorem, 8, 65
   1.233 -  \item {\tt disjL} theorem, 103
   1.234 -  \item {\tt disjR} theorem, 103
   1.235 -  \item {\tt div} symbol, 47, 78, 124
   1.236 -  \item {\tt div_def} theorem, 47, 124
   1.237 +  \item {\tt disjL} theorem, 106
   1.238 +  \item {\tt disjR} theorem, 106
   1.239 +  \item {\tt div} symbol, 47, 78, 127
   1.240 +  \item {\tt div_def} theorem, 47, 127
   1.241    \item {\tt div_geq} theorem, 79
   1.242    \item {\tt div_less} theorem, 79
   1.243 +  \item {\tt Divides} theory, 79
   1.244    \item {\tt domain} constant, 25, 39
   1.245    \item {\tt domain_def} theorem, 31
   1.246    \item {\tt domain_of_fun} theorem, 39
   1.247 @@ -229,28 +230,28 @@
   1.248  
   1.249    \indexspace
   1.250  
   1.251 -  \item {\tt Elem} constant, 113
   1.252 -  \item {\tt elim_rls}, \bold{120}
   1.253 -  \item {\tt elimL_rls}, \bold{120}
   1.254 +  \item {\tt Elem} constant, 116
   1.255 +  \item {\tt elim_rls}, \bold{123}
   1.256 +  \item {\tt elimL_rls}, \bold{123}
   1.257    \item {\tt empty_def} theorem, 71
   1.258 -  \item {\tt empty_pack}, \bold{106}
   1.259 +  \item {\tt empty_pack}, \bold{109}
   1.260    \item {\tt empty_subsetI} theorem, 33
   1.261    \item {\tt emptyE} theorem, 33, 73
   1.262    \item {\tt Eps} constant, 60, 62
   1.263 -  \item {\tt Eq} constant, 113
   1.264 -  \item {\tt eq} constant, 113, 118
   1.265 +  \item {\tt Eq} constant, 116
   1.266 +  \item {\tt eq} constant, 116, 121
   1.267    \item {\tt eq_mp_tac}, \bold{10}
   1.268 -  \item {\tt EqC} theorem, 119
   1.269 -  \item {\tt EqE} theorem, 119
   1.270 -  \item {\tt Eqelem} constant, 113
   1.271 -  \item {\tt EqF} theorem, 119
   1.272 -  \item {\tt EqFL} theorem, 119
   1.273 -  \item {\tt EqI} theorem, 119
   1.274 -  \item {\tt Eqtype} constant, 113
   1.275 -  \item {\tt equal_tac}, \bold{121}
   1.276 -  \item {\tt equal_types} theorem, 116
   1.277 -  \item {\tt equal_typesL} theorem, 116
   1.278 -  \item {\tt equalityCE} theorem, 70, 72, 98
   1.279 +  \item {\tt EqC} theorem, 122
   1.280 +  \item {\tt EqE} theorem, 122
   1.281 +  \item {\tt Eqelem} constant, 116
   1.282 +  \item {\tt EqF} theorem, 122
   1.283 +  \item {\tt EqFL} theorem, 122
   1.284 +  \item {\tt EqI} theorem, 122
   1.285 +  \item {\tt Eqtype} constant, 116
   1.286 +  \item {\tt equal_tac}, \bold{124}
   1.287 +  \item {\tt equal_types} theorem, 119
   1.288 +  \item {\tt equal_typesL} theorem, 119
   1.289 +  \item {\tt equalityCE} theorem, 70, 72, 101, 102
   1.290    \item {\tt equalityD1} theorem, 33, 72
   1.291    \item {\tt equalityD2} theorem, 33, 72
   1.292    \item {\tt equalityE} theorem, 33, 72
   1.293 @@ -259,8 +260,8 @@
   1.294    \item {\tt equals0I} theorem, 33
   1.295    \item {\tt eresolve_tac}, 16
   1.296    \item {\tt eta} theorem, 39, 40
   1.297 -  \item {\tt EX} symbol, 7, 26, 60, 62, 69, 70, 101
   1.298 -  \item {\tt Ex} constant, 7, 60, 101
   1.299 +  \item {\tt EX} symbol, 7, 26, 60, 62, 69, 70, 104
   1.300 +  \item {\tt Ex} constant, 7, 60, 104
   1.301    \item {\tt EX!} symbol, 7, 60
   1.302    \item {\tt Ex1} constant, 7, 60
   1.303    \item {\tt Ex1_def} theorem, 64
   1.304 @@ -274,27 +275,27 @@
   1.305    \item {\tt exE} theorem, 8, 66
   1.306    \item {\tt exhaust_tac}, \bold{88}
   1.307    \item {\tt exI} theorem, 8, 66
   1.308 -  \item {\tt exL} theorem, 103
   1.309 -  \item {\tt Exp} theory, 96
   1.310 +  \item {\tt exL} theorem, 106
   1.311 +  \item {\tt Exp} theory, 99
   1.312    \item {\tt expand_if} theorem, 66
   1.313    \item {\tt expand_split} theorem, 76
   1.314    \item {\tt expand_sum_case} theorem, 78
   1.315 -  \item {\tt exR} theorem, 103, 106, 108
   1.316 -  \item {\tt exR_thin} theorem, 104, 108, 109
   1.317 +  \item {\tt exR} theorem, 106, 109, 111
   1.318 +  \item {\tt exR_thin} theorem, 107, 111, 112
   1.319    \item {\tt ext} theorem, 63, 64
   1.320    \item {\tt extension} theorem, 30
   1.321  
   1.322    \indexspace
   1.323  
   1.324 -  \item {\tt F} constant, 113
   1.325 -  \item {\tt False} constant, 7, 60, 101
   1.326 +  \item {\tt F} constant, 116
   1.327 +  \item {\tt False} constant, 7, 60, 104
   1.328    \item {\tt False_def} theorem, 64
   1.329    \item {\tt FalseE} theorem, 8, 65
   1.330 -  \item {\tt FalseL} theorem, 103
   1.331 -  \item {\tt fast_tac}, \bold{108}
   1.332 -  \item {\tt FE} theorem, 119, 123
   1.333 -  \item {\tt FEL} theorem, 119
   1.334 -  \item {\tt FF} theorem, 119
   1.335 +  \item {\tt FalseL} theorem, 106
   1.336 +  \item {\tt fast_tac}, \bold{111}
   1.337 +  \item {\tt FE} theorem, 122, 126
   1.338 +  \item {\tt FEL} theorem, 122
   1.339 +  \item {\tt FF} theorem, 122
   1.340    \item {\tt field} constant, 25
   1.341    \item {\tt field_def} theorem, 31
   1.342    \item {\tt field_subset} theorem, 38
   1.343 @@ -302,8 +303,8 @@
   1.344    \item {\tt fieldE} theorem, 38
   1.345    \item {\tt fieldI1} theorem, 38
   1.346    \item {\tt fieldI2} theorem, 38
   1.347 -  \item {\tt filseq_resolve_tac}, \bold{106}
   1.348 -  \item {\tt filt_resolve_tac}, 106, 121
   1.349 +  \item {\tt filseq_resolve_tac}, \bold{109}
   1.350 +  \item {\tt filt_resolve_tac}, 109, 124
   1.351    \item {\tt filter} constant, 81
   1.352    \item {\tt Fin.consI} theorem, 48
   1.353    \item {\tt Fin.emptyI} theorem, 48
   1.354 @@ -316,20 +317,20 @@
   1.355    \item {\tt Fixedpt} theory, 42
   1.356    \item {\tt flat} constant, 49
   1.357    \item {\tt flat_def} theorem, 49
   1.358 -  \item flex-flex constraints, 100
   1.359 -  \item {\tt FOL} theory, 1, 5, 11, 122
   1.360 +  \item flex-flex constraints, 103
   1.361 +  \item {\tt FOL} theory, 1, 5, 11, 125
   1.362    \item {\tt FOL_cs}, \bold{11}
   1.363    \item {\tt FOL_ss}, \bold{6}
   1.364    \item {\tt foldl} constant, 81
   1.365 -  \item {\tt form_rls}, \bold{120}
   1.366 -  \item {\tt formL_rls}, \bold{120}
   1.367 -  \item {\tt forms_of_seq}, \bold{105}
   1.368 +  \item {\tt form_rls}, \bold{123}
   1.369 +  \item {\tt formL_rls}, \bold{123}
   1.370 +  \item {\tt forms_of_seq}, \bold{108}
   1.371    \item {\tt foundation} theorem, 30
   1.372 -  \item {\tt fst} constant, 25, 29, 76, 113, 118
   1.373 +  \item {\tt fst} constant, 25, 32, 76, 116, 121
   1.374    \item {\tt fst_conv} theorem, 37, 76
   1.375 -  \item {\tt fst_def} theorem, 31, 118
   1.376 +  \item {\tt fst_def} theorem, 31, 121
   1.377    \item {\tt Fun} theory, 75
   1.378 -  \item {\tt fun} type, 61
   1.379 +  \item {\textit {fun}} type, 61
   1.380    \item {\tt fun_cong} theorem, 65
   1.381    \item {\tt fun_disjoint_apply1} theorem, 40, 56
   1.382    \item {\tt fun_disjoint_apply2} theorem, 40
   1.383 @@ -339,7 +340,7 @@
   1.384    \item {\tt fun_is_rel} theorem, 39
   1.385    \item {\tt fun_single} theorem, 40
   1.386    \item function applications
   1.387 -    \subitem in \CTT, 115
   1.388 +    \subitem in \CTT, 118
   1.389      \subitem in \ZF, 25
   1.390  
   1.391    \indexspace
   1.392 @@ -355,7 +356,7 @@
   1.393    \indexspace
   1.394  
   1.395    \item {\tt hd} constant, 81
   1.396 -  \item higher-order logic, 59--99
   1.397 +  \item higher-order logic, 59--102
   1.398    \item {\tt HOL} theory, 1, 59
   1.399    \item {\sc hol} system, 59, 62
   1.400    \item {\tt HOL_basic_ss}, \bold{75}
   1.401 @@ -363,12 +364,12 @@
   1.402    \item {\tt HOL_quantifiers}, \bold{62}, 70
   1.403    \item {\tt HOL_ss}, \bold{75}
   1.404    \item {\tt HOLCF} theory, 1
   1.405 -  \item {\tt hyp_rew_tac}, \bold{122}
   1.406 +  \item {\tt hyp_rew_tac}, \bold{125}
   1.407    \item {\tt hyp_subst_tac}, 6, 75
   1.408  
   1.409    \indexspace
   1.410  
   1.411 -  \item {\tt i} type, 24, 112
   1.412 +  \item {\textit {i}} type, 24, 115
   1.413    \item {\tt id} constant, 45
   1.414    \item {\tt id_def} theorem, 45
   1.415    \item {\tt If} constant, 60
   1.416 @@ -378,15 +379,15 @@
   1.417    \item {\tt if_P} theorem, 35, 66
   1.418    \item {\tt ifE} theorem, 19
   1.419    \item {\tt iff} theorem, 63, 64
   1.420 -  \item {\tt iff_def} theorem, 8, 103
   1.421 +  \item {\tt iff_def} theorem, 8, 106
   1.422    \item {\tt iff_impE} theorem, 9
   1.423    \item {\tt iffCE} theorem, 11, 66, 70
   1.424    \item {\tt iffD1} theorem, 9, 65
   1.425    \item {\tt iffD2} theorem, 9, 65
   1.426    \item {\tt iffE} theorem, 9, 65
   1.427    \item {\tt iffI} theorem, 9, 19, 65
   1.428 -  \item {\tt iffL} theorem, 104, 110
   1.429 -  \item {\tt iffR} theorem, 104
   1.430 +  \item {\tt iffL} theorem, 107, 113
   1.431 +  \item {\tt iffR} theorem, 107
   1.432    \item {\tt ifI} theorem, 19
   1.433    \item {\tt IFOL} theory, 5
   1.434    \item {\tt IFOL_ss}, \bold{6}
   1.435 @@ -397,13 +398,13 @@
   1.436    \item {\tt impCE} theorem, 11, 66
   1.437    \item {\tt impE} theorem, 9, 10, 65
   1.438    \item {\tt impI} theorem, 8, 63
   1.439 -  \item {\tt impL} theorem, 103
   1.440 -  \item {\tt impR} theorem, 103
   1.441 +  \item {\tt impL} theorem, 106
   1.442 +  \item {\tt impR} theorem, 106
   1.443    \item {\tt in} symbol, 27, 61
   1.444 -  \item {\tt ind} type, 79
   1.445 +  \item {\textit {ind}} type, 79
   1.446    \item {\tt induct} theorem, 44
   1.447    \item {\tt induct_tac}, 80, \bold{88}
   1.448 -  \item {\tt inductive}, 92--95
   1.449 +  \item {\tt inductive}, 95--98
   1.450    \item {\tt Inf} constant, 25, 29
   1.451    \item {\tt infinity} theorem, 31
   1.452    \item {\tt inj} constant, 45, 75
   1.453 @@ -415,13 +416,13 @@
   1.454    \item {\tt inj_onto_def} theorem, 75
   1.455    \item {\tt inj_Suc} theorem, 78
   1.456    \item {\tt Inl} constant, 43, 78
   1.457 -  \item {\tt inl} constant, 113, 118, 128
   1.458 +  \item {\tt inl} constant, 116, 121, 131
   1.459    \item {\tt Inl_def} theorem, 43
   1.460    \item {\tt Inl_inject} theorem, 43
   1.461    \item {\tt Inl_neq_Inr} theorem, 43
   1.462    \item {\tt Inl_not_Inr} theorem, 78
   1.463    \item {\tt Inr} constant, 43, 78
   1.464 -  \item {\tt inr} constant, 113, 118
   1.465 +  \item {\tt inr} constant, 116, 121
   1.466    \item {\tt Inr_def} theorem, 43
   1.467    \item {\tt Inr_inject} theorem, 43
   1.468    \item {\tt insert} constant, 68
   1.469 @@ -467,21 +468,21 @@
   1.470    \item {\tt IntPr.safe_step_tac}, \bold{10}
   1.471    \item {\tt IntPr.safe_tac}, \bold{10}
   1.472    \item {\tt IntPr.step_tac}, \bold{10}
   1.473 -  \item {\tt intr_rls}, \bold{120}
   1.474 -  \item {\tt intr_tac}, \bold{121}, 130, 131
   1.475 -  \item {\tt intrL_rls}, \bold{120}
   1.476 +  \item {\tt intr_rls}, \bold{123}
   1.477 +  \item {\tt intr_tac}, \bold{124}, 133, 134
   1.478 +  \item {\tt intrL_rls}, \bold{123}
   1.479    \item {\tt inv} constant, 75
   1.480    \item {\tt inv_def} theorem, 75
   1.481  
   1.482    \indexspace
   1.483  
   1.484 -  \item {\tt lam} symbol, 26, 28, 115
   1.485 +  \item {\tt lam} symbol, 26, 28, 118
   1.486    \item {\tt lam_def} theorem, 31
   1.487    \item {\tt lam_type} theorem, 39
   1.488 -  \item {\tt Lambda} constant, 25, 28
   1.489 -  \item {\tt lambda} constant, 113, 115
   1.490 +  \item {\tt Lambda} constant, 25, 29
   1.491 +  \item {\tt lambda} constant, 116, 118
   1.492    \item $\lambda$-abstractions
   1.493 -    \subitem in \CTT, 115
   1.494 +    \subitem in \CTT, 118
   1.495      \subitem in \ZF, 26
   1.496    \item {\tt lamE} theorem, 39, 40
   1.497    \item {\tt lamI} theorem, 39, 40
   1.498 @@ -499,7 +500,7 @@
   1.499    \item {\tt Let} constant, 24, 25, 60, 63
   1.500    \item {\tt let} symbol, 27, 61, 63
   1.501    \item {\tt Let_def} theorem, 24, 30, 63, 64
   1.502 -  \item {\tt LFilter} theory, 96
   1.503 +  \item {\tt LFilter} theory, 99
   1.504    \item {\tt lfp_def} theorem, 44
   1.505    \item {\tt lfp_greatest} theorem, 44
   1.506    \item {\tt lfp_lowerbound} theorem, 44
   1.507 @@ -507,8 +508,9 @@
   1.508    \item {\tt lfp_subset} theorem, 44
   1.509    \item {\tt lfp_Tarski} theorem, 44
   1.510    \item {\tt List} theory, 80, 81
   1.511 +  \item {\textit {list}} type, 99
   1.512 +  \item {\textit{list}} type, 80
   1.513    \item {\tt list} constant, 49
   1.514 -  \item {\tt list} type, 80, 96
   1.515    \item {\tt List.induct} theorem, 49
   1.516    \item {\tt list_case} constant, 49
   1.517    \item {\tt list_mono} theorem, 49
   1.518 @@ -516,10 +518,10 @@
   1.519    \item {\tt list_rec_Cons} theorem, 49
   1.520    \item {\tt list_rec_def} theorem, 49
   1.521    \item {\tt list_rec_Nil} theorem, 49
   1.522 -  \item {\tt LK} theory, 1, 100, 104
   1.523 -  \item {\tt LK_dup_pack}, \bold{106}, 108
   1.524 -  \item {\tt LK_pack}, \bold{106}
   1.525 -  \item {\tt LList} theory, 96
   1.526 +  \item {\tt LK} theory, 1, 103, 107
   1.527 +  \item {\tt LK_dup_pack}, \bold{109}, 111
   1.528 +  \item {\tt LK_pack}, \bold{109}
   1.529 +  \item {\tt LList} theory, 99
   1.530    \item {\tt logic} class, 5
   1.531  
   1.532    \indexspace
   1.533 @@ -538,32 +540,33 @@
   1.534    \item {\tt mem_irrefl} theorem, 35
   1.535    \item {\tt min} constant, 61, 79
   1.536    \item {\tt minus} class, 61
   1.537 -  \item {\tt mod} symbol, 47, 78, 124
   1.538 -  \item {\tt mod_def} theorem, 47, 124
   1.539 +  \item {\tt mod} symbol, 47, 78, 127
   1.540 +  \item {\tt mod_def} theorem, 47, 127
   1.541    \item {\tt mod_geq} theorem, 79
   1.542    \item {\tt mod_less} theorem, 79
   1.543    \item {\tt mod_quo_equality} theorem, 47
   1.544    \item {\tt Modal} theory, 1
   1.545    \item {\tt mono} constant, 61
   1.546    \item {\tt mp} theorem, 8, 63
   1.547 -  \item {\tt mp_tac}, \bold{10}, \bold{122}
   1.548 +  \item {\tt mp_tac}, \bold{10}, \bold{125}
   1.549    \item {\tt mult_0} theorem, 47
   1.550 -  \item {\tt mult_assoc} theorem, 47, 124
   1.551 -  \item {\tt mult_commute} theorem, 47, 124
   1.552 -  \item {\tt mult_def} theorem, 47, 124
   1.553 +  \item {\tt mult_assoc} theorem, 47, 127
   1.554 +  \item {\tt mult_commute} theorem, 47, 127
   1.555 +  \item {\tt mult_def} theorem, 47, 127
   1.556    \item {\tt mult_succ} theorem, 47
   1.557    \item {\tt mult_type} theorem, 47
   1.558 -  \item {\tt mult_typing} theorem, 124
   1.559 -  \item {\tt multC0} theorem, 124
   1.560 -  \item {\tt multC_succ} theorem, 124
   1.561 +  \item {\tt mult_typing} theorem, 127
   1.562 +  \item {\tt multC0} theorem, 127
   1.563 +  \item {\tt multC_succ} theorem, 127
   1.564  
   1.565    \indexspace
   1.566  
   1.567 -  \item {\tt N} constant, 113
   1.568 +  \item {\tt N} constant, 116
   1.569    \item {\tt n_not_Suc_n} theorem, 78
   1.570    \item {\tt Nat} theory, 46, 79
   1.571 +  \item {\textit {nat}} type, 78, 79, 88
   1.572 +  \item {\textit{nat}} type, 79--80
   1.573    \item {\tt nat} constant, 47
   1.574 -  \item {\tt nat} type, 79
   1.575    \item {\tt nat_0I} theorem, 47
   1.576    \item {\tt nat_case} constant, 47
   1.577    \item {\tt nat_case_0} theorem, 47
   1.578 @@ -574,46 +577,46 @@
   1.579    \item {\tt nat_rec} constant, 80
   1.580    \item {\tt nat_succI} theorem, 47
   1.581    \item {\tt NatDef} theory, 79
   1.582 -  \item {\tt NC0} theorem, 117
   1.583 -  \item {\tt NC_succ} theorem, 117
   1.584 -  \item {\tt NE} theorem, 116, 117, 125
   1.585 -  \item {\tt NEL} theorem, 117
   1.586 -  \item {\tt NF} theorem, 117, 126
   1.587 -  \item {\tt NI0} theorem, 117
   1.588 -  \item {\tt NI_succ} theorem, 117
   1.589 -  \item {\tt NI_succL} theorem, 117
   1.590 +  \item {\tt NC0} theorem, 120
   1.591 +  \item {\tt NC_succ} theorem, 120
   1.592 +  \item {\tt NE} theorem, 119, 120, 128
   1.593 +  \item {\tt NEL} theorem, 120
   1.594 +  \item {\tt NF} theorem, 120, 129
   1.595 +  \item {\tt NI0} theorem, 120
   1.596 +  \item {\tt NI_succ} theorem, 120
   1.597 +  \item {\tt NI_succL} theorem, 120
   1.598    \item {\tt Nil_Cons_iff} theorem, 49
   1.599    \item {\tt NilI} theorem, 49
   1.600 -  \item {\tt NIO} theorem, 125
   1.601 -  \item {\tt Not} constant, 7, 60, 101
   1.602 +  \item {\tt NIO} theorem, 128
   1.603 +  \item {\tt Not} constant, 7, 60, 104
   1.604    \item {\tt not_def} theorem, 8, 42, 64
   1.605    \item {\tt not_impE} theorem, 9
   1.606    \item {\tt not_sym} theorem, 65
   1.607    \item {\tt notE} theorem, 9, 10, 65
   1.608    \item {\tt notI} theorem, 9, 65
   1.609 -  \item {\tt notL} theorem, 103
   1.610 +  \item {\tt notL} theorem, 106
   1.611    \item {\tt notnotD} theorem, 11, 66
   1.612 -  \item {\tt notR} theorem, 103
   1.613 +  \item {\tt notR} theorem, 106
   1.614    \item {\tt nth} constant, 81
   1.615    \item {\tt null} constant, 81
   1.616  
   1.617    \indexspace
   1.618  
   1.619    \item {\tt O} symbol, 45
   1.620 +  \item {\textit {o}} type, 5, 103
   1.621    \item {\tt o} symbol, 60, 71
   1.622 -  \item {\tt o} type, 5, 100
   1.623    \item {\tt o_def} theorem, 64
   1.624    \item {\tt of} symbol, 63
   1.625    \item {\tt or_def} theorem, 42, 64
   1.626    \item {\tt Ord} theory, 61
   1.627    \item {\tt ord} class, 61, 62, 79
   1.628 -  \item {\tt order} class, 61
   1.629 +  \item {\tt order} class, 61, 79
   1.630  
   1.631    \indexspace
   1.632  
   1.633 -  \item {\tt pack} ML type, 106
   1.634 +  \item {\tt pack} ML type, 109
   1.635    \item {\tt Pair} constant, 25, 26, 76
   1.636 -  \item {\tt pair} constant, 113
   1.637 +  \item {\tt pair} constant, 116
   1.638    \item {\tt Pair_def} theorem, 31
   1.639    \item {\tt Pair_eq} theorem, 76
   1.640    \item {\tt Pair_inject} theorem, 37, 76
   1.641 @@ -622,46 +625,46 @@
   1.642    \item {\tt Pair_neq_0} theorem, 37
   1.643    \item {\tt PairE} theorem, 76
   1.644    \item {\tt pairing} theorem, 34
   1.645 -  \item {\tt pc_tac}, \bold{107}, \bold{123}, 129, 130
   1.646 +  \item {\tt pc_tac}, \bold{110}, \bold{126}, 132, 133
   1.647    \item {\tt Perm} theory, 42
   1.648    \item {\tt Pi} constant, 25, 28, 40
   1.649    \item {\tt Pi_def} theorem, 31
   1.650    \item {\tt Pi_type} theorem, 39, 40
   1.651    \item {\tt plus} class, 61
   1.652 -  \item {\tt PlusC_inl} theorem, 119
   1.653 -  \item {\tt PlusC_inr} theorem, 119
   1.654 -  \item {\tt PlusE} theorem, 119, 123, 127
   1.655 -  \item {\tt PlusEL} theorem, 119
   1.656 -  \item {\tt PlusF} theorem, 119
   1.657 -  \item {\tt PlusFL} theorem, 119
   1.658 -  \item {\tt PlusI_inl} theorem, 119, 128
   1.659 -  \item {\tt PlusI_inlL} theorem, 119
   1.660 -  \item {\tt PlusI_inr} theorem, 119
   1.661 -  \item {\tt PlusI_inrL} theorem, 119
   1.662 +  \item {\tt PlusC_inl} theorem, 122
   1.663 +  \item {\tt PlusC_inr} theorem, 122
   1.664 +  \item {\tt PlusE} theorem, 122, 126, 130
   1.665 +  \item {\tt PlusEL} theorem, 122
   1.666 +  \item {\tt PlusF} theorem, 122
   1.667 +  \item {\tt PlusFL} theorem, 122
   1.668 +  \item {\tt PlusI_inl} theorem, 122, 131
   1.669 +  \item {\tt PlusI_inlL} theorem, 122
   1.670 +  \item {\tt PlusI_inr} theorem, 122
   1.671 +  \item {\tt PlusI_inrL} theorem, 122
   1.672    \item {\tt Pow} constant, 25, 68
   1.673    \item {\tt Pow_def} theorem, 71
   1.674    \item {\tt Pow_iff} theorem, 30
   1.675    \item {\tt Pow_mono} theorem, 52
   1.676    \item {\tt PowD} theorem, 33, 53, 73
   1.677    \item {\tt PowI} theorem, 33, 53, 73
   1.678 -  \item primitive recursion, 90--92
   1.679 -  \item {\tt primrec}, 90--92
   1.680 +  \item primitive recursion, 93
   1.681 +  \item {\tt primrec}, 91--92
   1.682    \item {\tt primrec} symbol, 79
   1.683    \item {\tt PrimReplace} constant, 25, 29
   1.684    \item priorities, 2
   1.685 -  \item {\tt PROD} symbol, 26, 28, 114, 115
   1.686 -  \item {\tt Prod} constant, 113
   1.687 +  \item {\tt PROD} symbol, 26, 28, 117, 118
   1.688 +  \item {\tt Prod} constant, 116
   1.689    \item {\tt Prod} theory, 76
   1.690 -  \item {\tt ProdC} theorem, 117, 133
   1.691 -  \item {\tt ProdC2} theorem, 117
   1.692 -  \item {\tt ProdE} theorem, 117, 130, 132, 134
   1.693 -  \item {\tt ProdEL} theorem, 117
   1.694 -  \item {\tt ProdF} theorem, 117
   1.695 -  \item {\tt ProdFL} theorem, 117
   1.696 -  \item {\tt ProdI} theorem, 117, 123, 125
   1.697 -  \item {\tt ProdIL} theorem, 117
   1.698 +  \item {\tt ProdC} theorem, 120, 136
   1.699 +  \item {\tt ProdC2} theorem, 120
   1.700 +  \item {\tt ProdE} theorem, 120, 133, 135, 137
   1.701 +  \item {\tt ProdEL} theorem, 120
   1.702 +  \item {\tt ProdF} theorem, 120
   1.703 +  \item {\tt ProdFL} theorem, 120
   1.704 +  \item {\tt ProdI} theorem, 120, 126, 128
   1.705 +  \item {\tt ProdIL} theorem, 120
   1.706    \item {\tt prop_cs}, \bold{11}, \bold{76}
   1.707 -  \item {\tt prop_pack}, \bold{106}
   1.708 +  \item {\tt prop_pack}, \bold{109}
   1.709  
   1.710    \indexspace
   1.711  
   1.712 @@ -683,38 +686,43 @@
   1.713  
   1.714    \indexspace
   1.715  
   1.716 -  \item {\tt range} constant, 25, 68, 97
   1.717 +  \item {\tt range} constant, 25, 68, 100
   1.718    \item {\tt range_def} theorem, 31, 71
   1.719    \item {\tt range_of_fun} theorem, 39, 40
   1.720    \item {\tt range_subset} theorem, 38
   1.721    \item {\tt range_type} theorem, 39
   1.722 -  \item {\tt rangeE} theorem, 38, 73, 97
   1.723 +  \item {\tt rangeE} theorem, 38, 73, 101
   1.724    \item {\tt rangeI} theorem, 38, 73
   1.725    \item {\tt rank} constant, 48
   1.726    \item {\tt rank_ss}, \bold{23}
   1.727 -  \item {\tt rec} constant, 47, 113, 116
   1.728 +  \item {\tt rec} constant, 47, 116, 119
   1.729    \item {\tt rec_0} theorem, 47
   1.730    \item {\tt rec_def} theorem, 47
   1.731    \item {\tt rec_succ} theorem, 47
   1.732 -  \item {\tt red_if_equal} theorem, 116
   1.733 -  \item {\tt Reduce} constant, 113, 116, 122
   1.734 -  \item {\tt refl} theorem, 8, 63, 103
   1.735 -  \item {\tt refl_elem} theorem, 116, 120
   1.736 -  \item {\tt refl_red} theorem, 116
   1.737 -  \item {\tt refl_type} theorem, 116, 120
   1.738 -  \item {\tt REPEAT_FIRST}, 121
   1.739 -  \item {\tt repeat_goal_tac}, \bold{107}
   1.740 +  \item {\tt recdef}, 93--95
   1.741 +  \item recursion
   1.742 +    \subitem general, 95
   1.743 +    \subitem primitive, 91--92
   1.744 +  \item recursive functions, \see{recursion}{90}
   1.745 +  \item {\tt red_if_equal} theorem, 119
   1.746 +  \item {\tt Reduce} constant, 116, 119, 125
   1.747 +  \item {\tt refl} theorem, 8, 63, 106
   1.748 +  \item {\tt refl_elem} theorem, 119, 123
   1.749 +  \item {\tt refl_red} theorem, 119
   1.750 +  \item {\tt refl_type} theorem, 119, 123
   1.751 +  \item {\tt REPEAT_FIRST}, 124
   1.752 +  \item {\tt repeat_goal_tac}, \bold{110}
   1.753    \item {\tt RepFun} constant, 25, 28, 29, 32
   1.754    \item {\tt RepFun_def} theorem, 30
   1.755    \item {\tt RepFunE} theorem, 34
   1.756    \item {\tt RepFunI} theorem, 34
   1.757    \item {\tt Replace} constant, 25, 28, 29, 32
   1.758    \item {\tt Replace_def} theorem, 30
   1.759 -  \item {\tt replace_type} theorem, 120, 132
   1.760 +  \item {\tt replace_type} theorem, 123, 135
   1.761    \item {\tt ReplaceE} theorem, 34
   1.762    \item {\tt ReplaceI} theorem, 34
   1.763    \item {\tt replacement} theorem, 30
   1.764 -  \item {\tt reresolve_tac}, \bold{107}
   1.765 +  \item {\tt reresolve_tac}, \bold{110}
   1.766    \item {\tt res_inst_tac}, 62
   1.767    \item {\tt restrict} constant, 25, 32
   1.768    \item {\tt restrict} theorem, 39
   1.769 @@ -723,32 +731,32 @@
   1.770    \item {\tt restrict_type} theorem, 39
   1.771    \item {\tt rev} constant, 49, 81
   1.772    \item {\tt rev_def} theorem, 49
   1.773 -  \item {\tt rew_tac}, 18, \bold{122}
   1.774 +  \item {\tt rew_tac}, 18, \bold{125}
   1.775    \item {\tt rewrite_rule}, 19
   1.776    \item {\tt right_comp_id} theorem, 45
   1.777    \item {\tt right_comp_inverse} theorem, 45
   1.778    \item {\tt right_inverse} theorem, 45
   1.779 -  \item {\tt RL}, 127
   1.780 -  \item {\tt RS}, 132, 134
   1.781 +  \item {\tt RL}, 130
   1.782 +  \item {\tt RS}, 135, 137
   1.783  
   1.784    \indexspace
   1.785  
   1.786 -  \item {\tt safe_goal_tac}, \bold{108}
   1.787 -  \item {\tt safe_tac}, \bold{123}
   1.788 -  \item {\tt safestep_tac}, \bold{123}
   1.789 +  \item {\tt safe_goal_tac}, \bold{111}
   1.790 +  \item {\tt safe_tac}, \bold{126}
   1.791 +  \item {\tt safestep_tac}, \bold{126}
   1.792    \item search
   1.793 -    \subitem best-first, 99
   1.794 +    \subitem best-first, 102
   1.795    \item {\tt select_equality} theorem, 64, 66
   1.796    \item {\tt selectI} theorem, 63, 64
   1.797    \item {\tt separation} theorem, 34
   1.798 -  \item {\tt Seqof} constant, 101
   1.799 -  \item sequent calculus, 100--111
   1.800 +  \item {\tt Seqof} constant, 104
   1.801 +  \item sequent calculus, 103--114
   1.802    \item {\tt Set} theory, 67, 70
   1.803 +  \item {\tt set} constant, 81
   1.804    \item {\tt set} type, 67
   1.805    \item set theory, 23--58
   1.806 -  \item {\tt set_current_thy}, 99
   1.807 +  \item {\tt set_current_thy}, 102
   1.808    \item {\tt set_diff_def} theorem, 71
   1.809 -  \item {\tt set_of_list} constant, 81
   1.810    \item {\tt show_sorts}, 62
   1.811    \item {\tt show_types}, 62
   1.812    \item {\tt Sigma} constant, 25, 28, 29, 37, 76
   1.813 @@ -761,19 +769,19 @@
   1.814    \item {\tt singletonE} theorem, 35
   1.815    \item {\tt singletonI} theorem, 35
   1.816    \item {\tt size} constant, 86
   1.817 -  \item {\tt snd} constant, 25, 29, 76, 113, 118
   1.818 +  \item {\tt snd} constant, 25, 32, 76, 116, 121
   1.819    \item {\tt snd_conv} theorem, 37, 76
   1.820 -  \item {\tt snd_def} theorem, 31, 118
   1.821 -  \item {\tt sobj} type, 102
   1.822 +  \item {\tt snd_def} theorem, 31, 121
   1.823 +  \item {\tt sobj} type, 105
   1.824    \item {\tt spec} theorem, 8, 66
   1.825 -  \item {\tt split} constant, 25, 29, 76, 113, 127
   1.826 +  \item {\tt split} constant, 25, 32, 76, 116, 130
   1.827    \item {\tt split} theorem, 37, 76
   1.828    \item {\tt split_all_tac}, \bold{77}
   1.829    \item {\tt split_def} theorem, 31
   1.830    \item {\tt ssubst} theorem, 9, 65, 67
   1.831    \item {\tt stac}, \bold{75}
   1.832    \item {\tt Step_tac}, 22
   1.833 -  \item {\tt step_tac}, 22, \bold{108}, \bold{123}
   1.834 +  \item {\tt step_tac}, 22, \bold{111}, \bold{126}
   1.835    \item {\tt strip_tac}, \bold{67}
   1.836    \item {\tt subset_def} theorem, 30, 71
   1.837    \item {\tt subset_refl} theorem, 33, 72
   1.838 @@ -782,15 +790,15 @@
   1.839    \item {\tt subsetD} theorem, 33, 55, 70, 72
   1.840    \item {\tt subsetI} theorem, 33, 53, 54, 72
   1.841    \item {\tt subst} theorem, 8, 63
   1.842 -  \item {\tt subst_elem} theorem, 116
   1.843 -  \item {\tt subst_elemL} theorem, 116
   1.844 -  \item {\tt subst_eqtyparg} theorem, 120, 132
   1.845 -  \item {\tt subst_prodE} theorem, 118, 120
   1.846 -  \item {\tt subst_type} theorem, 116
   1.847 -  \item {\tt subst_typeL} theorem, 116
   1.848 +  \item {\tt subst_elem} theorem, 119
   1.849 +  \item {\tt subst_elemL} theorem, 119
   1.850 +  \item {\tt subst_eqtyparg} theorem, 123, 135
   1.851 +  \item {\tt subst_prodE} theorem, 121, 123
   1.852 +  \item {\tt subst_type} theorem, 119
   1.853 +  \item {\tt subst_typeL} theorem, 119
   1.854    \item {\tt Suc} constant, 78
   1.855    \item {\tt Suc_not_Zero} theorem, 78
   1.856 -  \item {\tt succ} constant, 25, 29, 113
   1.857 +  \item {\tt succ} constant, 25, 29, 116
   1.858    \item {\tt succ_def} theorem, 31
   1.859    \item {\tt succ_inject} theorem, 35
   1.860    \item {\tt succ_neq_0} theorem, 35
   1.861 @@ -798,8 +806,8 @@
   1.862    \item {\tt succE} theorem, 35
   1.863    \item {\tt succI1} theorem, 35
   1.864    \item {\tt succI2} theorem, 35
   1.865 -  \item {\tt SUM} symbol, 26, 28, 114, 115
   1.866 -  \item {\tt Sum} constant, 113
   1.867 +  \item {\tt SUM} symbol, 26, 28, 117, 118
   1.868 +  \item {\tt Sum} constant, 116
   1.869    \item {\tt Sum} theory, 42, 77
   1.870    \item {\tt sum_case} constant, 78
   1.871    \item {\tt sum_case_Inl} theorem, 78
   1.872 @@ -811,70 +819,70 @@
   1.873    \item {\tt SUM_Int_distrib2} theorem, 41
   1.874    \item {\tt SUM_Un_distrib1} theorem, 41
   1.875    \item {\tt SUM_Un_distrib2} theorem, 41
   1.876 -  \item {\tt SumC} theorem, 118
   1.877 -  \item {\tt SumE} theorem, 118, 123, 127
   1.878 +  \item {\tt SumC} theorem, 121
   1.879 +  \item {\tt SumE} theorem, 121, 126, 130
   1.880    \item {\tt sumE} theorem, 78
   1.881    \item {\tt sumE2} theorem, 43
   1.882 -  \item {\tt SumE_fst} theorem, 118, 120, 132, 133
   1.883 -  \item {\tt SumE_snd} theorem, 118, 120, 134
   1.884 -  \item {\tt SumEL} theorem, 118
   1.885 -  \item {\tt SumF} theorem, 118
   1.886 -  \item {\tt SumFL} theorem, 118
   1.887 -  \item {\tt SumI} theorem, 118, 128
   1.888 -  \item {\tt SumIL} theorem, 118
   1.889 -  \item {\tt SumIL2} theorem, 120
   1.890 +  \item {\tt SumE_fst} theorem, 121, 123, 135, 136
   1.891 +  \item {\tt SumE_snd} theorem, 121, 123, 137
   1.892 +  \item {\tt SumEL} theorem, 121
   1.893 +  \item {\tt SumF} theorem, 121
   1.894 +  \item {\tt SumFL} theorem, 121
   1.895 +  \item {\tt SumI} theorem, 121, 131
   1.896 +  \item {\tt SumIL} theorem, 121
   1.897 +  \item {\tt SumIL2} theorem, 123
   1.898    \item {\tt surj} constant, 45, 71, 75
   1.899    \item {\tt surj_def} theorem, 45, 75
   1.900    \item {\tt surjective_pairing} theorem, 76
   1.901    \item {\tt surjective_sum} theorem, 78
   1.902    \item {\tt swap} theorem, 11, 66
   1.903 -  \item {\tt swap_res_tac}, 16, 98
   1.904 -  \item {\tt sym} theorem, 9, 65, 103
   1.905 -  \item {\tt sym_elem} theorem, 116
   1.906 -  \item {\tt sym_type} theorem, 116
   1.907 -  \item {\tt symL} theorem, 104
   1.908 +  \item {\tt swap_res_tac}, 16, 102
   1.909 +  \item {\tt sym} theorem, 9, 65, 106
   1.910 +  \item {\tt sym_elem} theorem, 119
   1.911 +  \item {\tt sym_type} theorem, 119
   1.912 +  \item {\tt symL} theorem, 107
   1.913  
   1.914    \indexspace
   1.915  
   1.916 -  \item {\tt T} constant, 113
   1.917 -  \item {\tt t} type, 112
   1.918 +  \item {\tt T} constant, 116
   1.919 +  \item {\textit {t}} type, 115
   1.920    \item {\tt take} constant, 81
   1.921    \item {\tt takeWhile} constant, 81
   1.922 -  \item {\tt TC} theorem, 119
   1.923 -  \item {\tt TE} theorem, 119
   1.924 -  \item {\tt TEL} theorem, 119
   1.925 -  \item {\tt term} class, 5, 61, 100
   1.926 -  \item {\tt test_assume_tac}, \bold{121}
   1.927 -  \item {\tt TF} theorem, 119
   1.928 -  \item {\tt THE} symbol, 26, 28, 36, 101
   1.929 -  \item {\tt The} constant, 25, 28, 29, 101
   1.930 -  \item {\tt The} theorem, 103
   1.931 +  \item {\tt TC} theorem, 122
   1.932 +  \item {\tt TE} theorem, 122
   1.933 +  \item {\tt TEL} theorem, 122
   1.934 +  \item {\tt term} class, 5, 61, 103
   1.935 +  \item {\tt test_assume_tac}, \bold{124}
   1.936 +  \item {\tt TF} theorem, 122
   1.937 +  \item {\tt THE} symbol, 26, 28, 36, 104
   1.938 +  \item {\tt The} constant, 25, 28, 29, 104
   1.939 +  \item {\tt The} theorem, 106
   1.940    \item {\tt the_def} theorem, 30
   1.941    \item {\tt the_equality} theorem, 35, 36
   1.942    \item {\tt theI} theorem, 35, 36
   1.943 -  \item {\tt thinL} theorem, 103
   1.944 -  \item {\tt thinR} theorem, 103
   1.945 -  \item {\tt TI} theorem, 119
   1.946 +  \item {\tt thinL} theorem, 106
   1.947 +  \item {\tt thinR} theorem, 106
   1.948 +  \item {\tt TI} theorem, 122
   1.949    \item {\tt times} class, 61
   1.950    \item {\tt tl} constant, 81
   1.951    \item tracing
   1.952      \subitem of unification, 62
   1.953 -  \item {\tt trans} theorem, 9, 65, 103
   1.954 -  \item {\tt trans_elem} theorem, 116
   1.955 -  \item {\tt trans_red} theorem, 116
   1.956 +  \item {\tt trans} theorem, 9, 65, 106
   1.957 +  \item {\tt trans_elem} theorem, 119
   1.958 +  \item {\tt trans_red} theorem, 119
   1.959    \item {\tt trans_tac}, 80
   1.960 -  \item {\tt trans_type} theorem, 116
   1.961 -  \item {\tt True} constant, 7, 60, 101
   1.962 -  \item {\tt True_def} theorem, 8, 64, 103
   1.963 +  \item {\tt trans_type} theorem, 119
   1.964 +  \item {\tt True} constant, 7, 60, 104
   1.965 +  \item {\tt True_def} theorem, 8, 64, 106
   1.966    \item {\tt True_or_False} theorem, 63, 64
   1.967    \item {\tt TrueI} theorem, 9, 65
   1.968 -  \item {\tt Trueprop} constant, 7, 60, 101
   1.969 -  \item {\tt TrueR} theorem, 104
   1.970 -  \item {\tt tt} constant, 113
   1.971 +  \item {\tt Trueprop} constant, 7, 60, 104
   1.972 +  \item {\tt TrueR} theorem, 107
   1.973 +  \item {\tt tt} constant, 116
   1.974    \item {\tt ttl} constant, 81
   1.975 -  \item {\tt Type} constant, 113
   1.976 +  \item {\tt Type} constant, 116
   1.977    \item type definition, \bold{83}
   1.978 -  \item {\tt typechk_tac}, \bold{121}, 126, 129, 133, 134
   1.979 +  \item {\tt typechk_tac}, \bold{124}, 129, 132, 136, 137
   1.980    \item {\tt typedef}, 80
   1.981  
   1.982    \indexspace
   1.983 @@ -931,7 +939,7 @@
   1.984  
   1.985    \indexspace
   1.986  
   1.987 -  \item {\tt when} constant, 113, 118, 127
   1.988 +  \item {\tt when} constant, 116, 121, 130
   1.989  
   1.990    \indexspace
   1.991  
   1.992 @@ -939,7 +947,7 @@
   1.993  
   1.994    \indexspace
   1.995  
   1.996 -  \item {\tt zero_ne_succ} theorem, 116, 117
   1.997 +  \item {\tt zero_ne_succ} theorem, 119, 120
   1.998    \item {\tt ZF} theory, 1, 23, 59
   1.999    \item {\tt ZF_cs}, \bold{23}
  1.1000    \item {\tt ZF_ss}, \bold{23}
     2.1 --- a/doc-src/Ref/ref.ind	Fri Jul 04 12:32:31 1997 +0200
     2.2 +++ b/doc-src/Ref/ref.ind	Fri Jul 04 12:36:00 1997 +0200
     2.3 @@ -153,7 +153,7 @@
     2.4    \item {\tt commit}, \bold{2}
     2.5    \item {\tt COMP}, \bold{46}
     2.6    \item {\tt compose}, \bold{46}
     2.7 -  \item {\tt compose_tac}, \bold{22}
     2.8 +  \item {\tt compose_tac}, \bold{23}
     2.9    \item {\tt compSWrapper}, \bold{124}
    2.10    \item {\tt compWrapper}, \bold{124}
    2.11    \item {\tt concl_of}, \bold{39}
    2.12 @@ -206,11 +206,14 @@
    2.13    \item destruct-resolution, 17
    2.14    \item {\tt DETERM}, \bold{32}
    2.15    \item discrimination nets, \bold{24}
    2.16 +  \item {\tt distinct_subgoals_tac}, \bold{22}
    2.17    \item {\tt dmatch_tac}, \bold{17}
    2.18    \item {\tt dres_inst_tac}, \bold{18}
    2.19    \item {\tt dresolve_tac}, \bold{17}
    2.20    \item {\tt dtac}, \bold{19}
    2.21    \item {\tt dummyT}, 82, 83, 93
    2.22 +  \item duplicate subgoals
    2.23 +    \subitem removing, 22
    2.24  
    2.25    \indexspace
    2.26  
    2.27 @@ -289,7 +292,7 @@
    2.28    \item {\tt frs}, \bold{11}
    2.29    \item {\tt Full_simp_tac}, \bold{100}, 105
    2.30    \item {\tt full_simp_tac}, 105, \bold{106}
    2.31 -  \item {\tt fun} type, 60
    2.32 +  \item {\textit {fun}} type, 60
    2.33    \item function applications, \bold{57}
    2.34  
    2.35    \indexspace
    2.36 @@ -404,7 +407,7 @@
    2.37  
    2.38    \indexspace
    2.39  
    2.40 -  \item {\tt o} type, 76
    2.41 +  \item {\textit {o}} type, 76
    2.42    \item {\tt op} symbol, 73
    2.43    \item {\tt option} ML type, 26
    2.44    \item oracles, 61--62
    2.45 @@ -470,8 +473,8 @@
    2.46      \subitem starting, 6
    2.47      \subitem timing, 10
    2.48    \item {\tt PROP} symbol, 65
    2.49 +  \item {\textit {prop}} type, 60, 66
    2.50    \item {\tt prop} nonterminal, \bold{64}, 76
    2.51 -  \item {\tt prop} type, 60, 66
    2.52    \item {\tt prove_goal}, 10, \bold{13}
    2.53    \item {\tt prove_goalw}, \bold{13}
    2.54    \item {\tt prove_goalw_cterm}, \bold{13}
    2.55 @@ -767,8 +770,8 @@
    2.56    \item {\tt tvar} nonterminal, \bold{66, 67}, 80, 87
    2.57    \item {\tt typ} ML type, 60
    2.58    \item {\tt Type}, \bold{60}
    2.59 +  \item {\textit {type}} type, 71
    2.60    \item {\tt type} nonterminal, \bold{66}
    2.61 -  \item {\tt type} type, 71
    2.62    \item type constraints, 66, 74, 83
    2.63    \item type constructors, \bold{60}
    2.64    \item type identifiers, 66