25 \indexspace |
25 \indexspace |
26 |
26 |
27 \item {\tt add_0} theorem, 45 |
27 \item {\tt add_0} theorem, 45 |
28 \item {\tt add_mult_dist} theorem, 45 |
28 \item {\tt add_mult_dist} theorem, 45 |
29 \item {\tt add_succ} theorem, 45 |
29 \item {\tt add_succ} theorem, 45 |
|
30 \item {\tt AddTCs}, \bold{49} |
|
31 \item {\tt addTCs}, \bold{49} |
30 \item {\tt ALL} symbol, 5, 25 |
32 \item {\tt ALL} symbol, 5, 25 |
31 \item {\tt All} constant, 5 |
33 \item {\tt All} constant, 5 |
32 \item {\tt all_dupE} theorem, 3, 7 |
34 \item {\tt all_dupE} theorem, 3, 7 |
33 \item {\tt all_impE} theorem, 7 |
35 \item {\tt all_impE} theorem, 7 |
34 \item {\tt allE} theorem, 3, 7 |
36 \item {\tt allE} theorem, 3, 7 |
35 \item {\tt allI} theorem, 6 |
37 \item {\tt allI} theorem, 6 |
36 \item {\tt and_def} theorem, 41 |
38 \item {\tt and_def} theorem, 41 |
37 \item {\tt apply_def} theorem, 29 |
39 \item {\tt apply_def} theorem, 29 |
38 \item {\tt apply_equality} theorem, 38, 39, 69 |
40 \item {\tt apply_equality} theorem, 38, 39, 70, 71 |
39 \item {\tt apply_equality2} theorem, 38 |
41 \item {\tt apply_equality2} theorem, 38 |
40 \item {\tt apply_iff} theorem, 38 |
42 \item {\tt apply_iff} theorem, 38 |
41 \item {\tt apply_Pair} theorem, 38, 69 |
43 \item {\tt apply_Pair} theorem, 38, 71 |
42 \item {\tt apply_type} theorem, 38 |
44 \item {\tt apply_type} theorem, 38 |
43 \item {\tt Arith} theory, 42 |
45 \item {\tt Arith} theory, 42 |
44 \item assumptions |
46 \item assumptions |
45 \subitem contradictory, 14 |
47 \subitem contradictory, 14 |
46 |
48 |
60 \item {\tt bexI} theorem, 31 |
62 \item {\tt bexI} theorem, 31 |
61 \item {\tt bij} constant, 44 |
63 \item {\tt bij} constant, 44 |
62 \item {\tt bij_converse_bij} theorem, 44 |
64 \item {\tt bij_converse_bij} theorem, 44 |
63 \item {\tt bij_def} theorem, 44 |
65 \item {\tt bij_def} theorem, 44 |
64 \item {\tt bij_disjoint_Un} theorem, 44 |
66 \item {\tt bij_disjoint_Un} theorem, 44 |
65 \item {\tt Blast_tac}, 15, 67, 68 |
67 \item {\tt Blast_tac}, 15, 68, 69 |
66 \item {\tt blast_tac}, 16, 17, 19 |
68 \item {\tt blast_tac}, 16, 17, 19 |
67 \item {\tt bnd_mono_def} theorem, 43 |
69 \item {\tt bnd_mono_def} theorem, 43 |
68 \item {\tt Bool} theory, 39 |
70 \item {\tt Bool} theory, 39 |
69 \item {\tt bool_0I} theorem, 41 |
71 \item {\tt bool_0I} theorem, 41 |
70 \item {\tt bool_1I} theorem, 41 |
72 \item {\tt bool_1I} theorem, 41 |
77 \item {\tt case} constant, 41 |
79 \item {\tt case} constant, 41 |
78 \item {\tt case_def} theorem, 41 |
80 \item {\tt case_def} theorem, 41 |
79 \item {\tt case_Inl} theorem, 41 |
81 \item {\tt case_Inl} theorem, 41 |
80 \item {\tt case_Inr} theorem, 41 |
82 \item {\tt case_Inr} theorem, 41 |
81 \item {\tt coinduct} theorem, 43 |
83 \item {\tt coinduct} theorem, 43 |
82 \item {\tt coinductive}, 57--62 |
84 \item {\tt coinductive}, 58--63 |
83 \item {\tt Collect} constant, 24, 25, 30 |
85 \item {\tt Collect} constant, 24, 25, 30 |
84 \item {\tt Collect_def} theorem, 28 |
86 \item {\tt Collect_def} theorem, 28 |
85 \item {\tt Collect_subset} theorem, 35 |
87 \item {\tt Collect_subset} theorem, 35 |
86 \item {\tt CollectD1} theorem, 32, 33 |
88 \item {\tt CollectD1} theorem, 32, 33 |
87 \item {\tt CollectD2} theorem, 32, 33 |
89 \item {\tt CollectD2} theorem, 32, 33 |
117 \item {\tt converse_def} theorem, 29 |
119 \item {\tt converse_def} theorem, 29 |
118 \item {\tt cut_facts_tac}, 17 |
120 \item {\tt cut_facts_tac}, 17 |
119 |
121 |
120 \indexspace |
122 \indexspace |
121 |
123 |
122 \item {\tt datatype}, 48--55 |
124 \item {\tt datatype}, 49--56 |
|
125 \item {\tt DelTCs}, \bold{49} |
|
126 \item {\tt delTCs}, \bold{49} |
123 \item {\tt Diff_cancel} theorem, 40 |
127 \item {\tt Diff_cancel} theorem, 40 |
124 \item {\tt Diff_contains} theorem, 35 |
128 \item {\tt Diff_contains} theorem, 35 |
125 \item {\tt Diff_def} theorem, 28 |
129 \item {\tt Diff_def} theorem, 28 |
126 \item {\tt Diff_disjoint} theorem, 40 |
130 \item {\tt Diff_disjoint} theorem, 40 |
127 \item {\tt Diff_Int} theorem, 40 |
131 \item {\tt Diff_Int} theorem, 40 |
145 \item {\tt domain_subset} theorem, 37 |
149 \item {\tt domain_subset} theorem, 37 |
146 \item {\tt domain_type} theorem, 38 |
150 \item {\tt domain_type} theorem, 38 |
147 \item {\tt domainE} theorem, 37 |
151 \item {\tt domainE} theorem, 37 |
148 \item {\tt domainI} theorem, 37 |
152 \item {\tt domainI} theorem, 37 |
149 \item {\tt double_complement} theorem, 40 |
153 \item {\tt double_complement} theorem, 40 |
150 \item {\tt dresolve_tac}, 66 |
154 \item {\tt dresolve_tac}, 67 |
151 |
155 |
152 \indexspace |
156 \indexspace |
153 |
157 |
154 \item {\tt empty_subsetI} theorem, 31 |
158 \item {\tt empty_subsetI} theorem, 31 |
155 \item {\tt emptyE} theorem, 31 |
159 \item {\tt emptyE} theorem, 31 |
156 \item {\tt eq_mp_tac}, \bold{8} |
160 \item {\tt eq_mp_tac}, \bold{8} |
157 \item {\tt equalityD1} theorem, 31 |
161 \item {\tt equalityD1} theorem, 31 |
158 \item {\tt equalityD2} theorem, 31 |
162 \item {\tt equalityD2} theorem, 31 |
159 \item {\tt equalityE} theorem, 31 |
163 \item {\tt equalityE} theorem, 31 |
160 \item {\tt equalityI} theorem, 31, 65 |
164 \item {\tt equalityI} theorem, 31, 66 |
161 \item {\tt equals0D} theorem, 31 |
165 \item {\tt equals0D} theorem, 31 |
162 \item {\tt equals0I} theorem, 31 |
166 \item {\tt equals0I} theorem, 31 |
163 \item {\tt eresolve_tac}, 14 |
167 \item {\tt eresolve_tac}, 14 |
164 \item {\tt eta} theorem, 38, 39 |
168 \item {\tt eta} theorem, 38, 39 |
165 \item {\tt EX} symbol, 5, 25 |
169 \item {\tt EX} symbol, 5, 25 |
166 \item {\tt Ex} constant, 5 |
170 \item {\tt Ex} constant, 5 |
167 \item {\tt EX!} symbol, 5 |
171 \item {\tt EX!} symbol, 5 |
168 \item {\tt ex/Term} theory, 49 |
172 \item {\tt ex/Term} theory, 51 |
169 \item {\tt Ex1} constant, 5 |
173 \item {\tt Ex1} constant, 5 |
170 \item {\tt ex1_def} theorem, 6 |
174 \item {\tt ex1_def} theorem, 6 |
171 \item {\tt ex1E} theorem, 7 |
175 \item {\tt ex1E} theorem, 7 |
172 \item {\tt ex1I} theorem, 7 |
176 \item {\tt ex1I} theorem, 7 |
173 \item {\tt ex_impE} theorem, 7 |
177 \item {\tt ex_impE} theorem, 7 |
174 \item {\tt exCI} theorem, 9, 13 |
178 \item {\tt exCI} theorem, 9, 13 |
175 \item {\tt excluded_middle} theorem, 9 |
179 \item {\tt excluded_middle} theorem, 9 |
176 \item {\tt exE} theorem, 6 |
180 \item {\tt exE} theorem, 6 |
177 \item {\tt exhaust_tac}, \bold{51} |
181 \item {\tt exhaust_tac}, \bold{54} |
178 \item {\tt exI} theorem, 6 |
182 \item {\tt exI} theorem, 6 |
179 \item {\tt extension} theorem, 28 |
183 \item {\tt extension} theorem, 28 |
180 |
184 |
181 \indexspace |
185 \indexspace |
182 |
186 |
199 \item first-order logic, 3--21 |
203 \item first-order logic, 3--21 |
200 \item {\tt Fixedpt} theory, 42 |
204 \item {\tt Fixedpt} theory, 42 |
201 \item {\tt flat} constant, 47 |
205 \item {\tt flat} constant, 47 |
202 \item {\tt FOL} theory, 3, 9 |
206 \item {\tt FOL} theory, 3, 9 |
203 \item {\tt FOL_cs}, \bold{9}, 48 |
207 \item {\tt FOL_cs}, \bold{9}, 48 |
204 \item {\tt FOL_ss}, \bold{4}, 46 |
208 \item {\tt FOL_ss}, \bold{4}, 48 |
205 \item {\tt foundation} theorem, 28 |
209 \item {\tt foundation} theorem, 28 |
206 \item {\tt fst} constant, 24, 30 |
210 \item {\tt fst} constant, 24, 30 |
207 \item {\tt fst_conv} theorem, 36 |
211 \item {\tt fst_conv} theorem, 36 |
208 \item {\tt fst_def} theorem, 29 |
212 \item {\tt fst_def} theorem, 29 |
209 \item {\tt fun_disjoint_apply1} theorem, 38, 69 |
213 \item {\tt fun_disjoint_apply1} theorem, 38, 70 |
210 \item {\tt fun_disjoint_apply2} theorem, 38 |
214 \item {\tt fun_disjoint_apply2} theorem, 38 |
211 \item {\tt fun_disjoint_Un} theorem, 38, 70 |
215 \item {\tt fun_disjoint_Un} theorem, 38, 71 |
212 \item {\tt fun_empty} theorem, 38 |
216 \item {\tt fun_empty} theorem, 38 |
213 \item {\tt fun_extension} theorem, 38, 39 |
217 \item {\tt fun_extension} theorem, 38, 39 |
214 \item {\tt fun_is_rel} theorem, 38 |
218 \item {\tt fun_is_rel} theorem, 38 |
215 \item {\tt fun_single} theorem, 38 |
219 \item {\tt fun_single} theorem, 38 |
216 \item function applications |
220 \item function applications |
257 \item {\tt impCE} theorem, 9 |
261 \item {\tt impCE} theorem, 9 |
258 \item {\tt impE} theorem, 7, 8 |
262 \item {\tt impE} theorem, 7, 8 |
259 \item {\tt impI} theorem, 6 |
263 \item {\tt impI} theorem, 6 |
260 \item {\tt in} symbol, 26 |
264 \item {\tt in} symbol, 26 |
261 \item {\tt induct} theorem, 43 |
265 \item {\tt induct} theorem, 43 |
262 \item {\tt induct_tac}, \bold{51} |
266 \item {\tt induct_tac}, \bold{53} |
263 \item {\tt inductive}, 57--62 |
267 \item {\tt inductive}, 58--63 |
264 \item {\tt Inf} constant, 24, 30 |
268 \item {\tt Inf} constant, 24, 30 |
265 \item {\tt infinity} theorem, 29 |
269 \item {\tt infinity} theorem, 29 |
266 \item {\tt inj} constant, 44 |
270 \item {\tt inj} constant, 44 |
267 \item {\tt inj_converse_inj} theorem, 44 |
271 \item {\tt inj_converse_inj} theorem, 44 |
268 \item {\tt inj_def} theorem, 44 |
272 \item {\tt inj_def} theorem, 44 |
278 \item {\tt Int_absorb} theorem, 40 |
282 \item {\tt Int_absorb} theorem, 40 |
279 \item {\tt Int_assoc} theorem, 40 |
283 \item {\tt Int_assoc} theorem, 40 |
280 \item {\tt Int_commute} theorem, 40 |
284 \item {\tt Int_commute} theorem, 40 |
281 \item {\tt Int_def} theorem, 28 |
285 \item {\tt Int_def} theorem, 28 |
282 \item {\tt INT_E} theorem, 33 |
286 \item {\tt INT_E} theorem, 33 |
283 \item {\tt Int_greatest} theorem, 35, 65, 66 |
287 \item {\tt Int_greatest} theorem, 35, 66, 68 |
284 \item {\tt INT_I} theorem, 33 |
288 \item {\tt INT_I} theorem, 33 |
285 \item {\tt Int_lower1} theorem, 35, 65 |
289 \item {\tt Int_lower1} theorem, 35, 67 |
286 \item {\tt Int_lower2} theorem, 35, 65 |
290 \item {\tt Int_lower2} theorem, 35, 67 |
287 \item {\tt Int_Un_distrib} theorem, 40 |
291 \item {\tt Int_Un_distrib} theorem, 40 |
288 \item {\tt Int_Union_RepFun} theorem, 40 |
292 \item {\tt Int_Union_RepFun} theorem, 40 |
289 \item {\tt IntD1} theorem, 34 |
293 \item {\tt IntD1} theorem, 34 |
290 \item {\tt IntD2} theorem, 34 |
294 \item {\tt IntD2} theorem, 34 |
291 \item {\tt IntE} theorem, 34, 66 |
295 \item {\tt IntE} theorem, 34, 67 |
292 \item {\tt Inter} constant, 24 |
296 \item {\tt Inter} constant, 24 |
293 \item {\tt Inter_def} theorem, 28 |
297 \item {\tt Inter_def} theorem, 28 |
294 \item {\tt Inter_greatest} theorem, 35 |
298 \item {\tt Inter_greatest} theorem, 35 |
295 \item {\tt Inter_lower} theorem, 35 |
299 \item {\tt Inter_lower} theorem, 35 |
296 \item {\tt Inter_Un_distrib} theorem, 40 |
300 \item {\tt Inter_Un_distrib} theorem, 40 |
343 \item {\tt map_flat} theorem, 47 |
347 \item {\tt map_flat} theorem, 47 |
344 \item {\tt map_ident} theorem, 47 |
348 \item {\tt map_ident} theorem, 47 |
345 \item {\tt map_type} theorem, 47 |
349 \item {\tt map_type} theorem, 47 |
346 \item {\tt mem_asym} theorem, 34, 35 |
350 \item {\tt mem_asym} theorem, 34, 35 |
347 \item {\tt mem_irrefl} theorem, 34 |
351 \item {\tt mem_irrefl} theorem, 34 |
348 \item {\tt mk_cases}, 54, 61 |
352 \item {\tt mk_cases}, 56, 63 |
349 \item {\tt mod} symbol, 45 |
353 \item {\tt mod} symbol, 45 |
350 \item {\tt mod_def} theorem, 45 |
354 \item {\tt mod_def} theorem, 45 |
351 \item {\tt mod_quo_equality} theorem, 45 |
355 \item {\tt mod_quo_equality} theorem, 45 |
352 \item {\tt mp} theorem, 6 |
356 \item {\tt mp} theorem, 6 |
353 \item {\tt mp_tac}, \bold{8} |
357 \item {\tt mp_tac}, \bold{8} |
397 \item {\tt Pi} constant, 24, 27, 39 |
401 \item {\tt Pi} constant, 24, 27, 39 |
398 \item {\tt Pi_def} theorem, 29 |
402 \item {\tt Pi_def} theorem, 29 |
399 \item {\tt Pi_type} theorem, 38, 39 |
403 \item {\tt Pi_type} theorem, 38, 39 |
400 \item {\tt Pow} constant, 24 |
404 \item {\tt Pow} constant, 24 |
401 \item {\tt Pow_iff} theorem, 28 |
405 \item {\tt Pow_iff} theorem, 28 |
402 \item {\tt Pow_mono} theorem, 65 |
406 \item {\tt Pow_mono} theorem, 66 |
403 \item {\tt PowD} theorem, 31, 66 |
407 \item {\tt PowD} theorem, 31, 67 |
404 \item {\tt PowI} theorem, 31, 66 |
408 \item {\tt PowI} theorem, 31, 67 |
405 \item {\tt primrec}, 55--57 |
409 \item {\tt primrec}, 57--58 |
406 \item {\tt PrimReplace} constant, 24, 30 |
410 \item {\tt PrimReplace} constant, 24, 30 |
407 \item priorities, 1 |
411 \item priorities, 1 |
408 \item {\tt PROD} symbol, 25, 27 |
412 \item {\tt PROD} symbol, 25, 27 |
409 \item {\tt prop_cs}, \bold{9} |
413 \item {\tt prop_cs}, \bold{9} |
410 |
414 |
411 \indexspace |
415 \indexspace |
412 |
416 |
413 \item {\tt qcase_def} theorem, 42 |
417 \item {\tt qcase_def} theorem, 42 |
414 \item {\tt qconverse} constant, 39 |
418 \item {\tt qconverse} constant, 39 |
415 \item {\tt qconverse_def} theorem, 42 |
419 \item {\tt qconverse_def} theorem, 42 |
416 \item {\tt qed_spec_mp}, 54 |
420 \item {\tt qed_spec_mp}, 55 |
417 \item {\tt qfsplit_def} theorem, 42 |
421 \item {\tt qfsplit_def} theorem, 42 |
418 \item {\tt QInl_def} theorem, 42 |
422 \item {\tt QInl_def} theorem, 42 |
419 \item {\tt QInr_def} theorem, 42 |
423 \item {\tt QInr_def} theorem, 42 |
420 \item {\tt QPair} theory, 39 |
424 \item {\tt QPair} theory, 39 |
421 \item {\tt QPair_def} theorem, 42 |
425 \item {\tt QPair_def} theorem, 42 |
433 \item {\tt range_of_fun} theorem, 38, 39 |
437 \item {\tt range_of_fun} theorem, 38, 39 |
434 \item {\tt range_subset} theorem, 37 |
438 \item {\tt range_subset} theorem, 37 |
435 \item {\tt range_type} theorem, 38 |
439 \item {\tt range_type} theorem, 38 |
436 \item {\tt rangeE} theorem, 37 |
440 \item {\tt rangeE} theorem, 37 |
437 \item {\tt rangeI} theorem, 37 |
441 \item {\tt rangeI} theorem, 37 |
438 \item {\tt rank} constant, 62 |
442 \item {\tt rank} constant, 63 |
439 \item recursion |
443 \item recursion |
440 \subitem primitive, 57 |
444 \subitem primitive, 57--58 |
441 \item recursive functions, \see{recursion}{55} |
445 \item recursive functions, \see{recursion}{57} |
442 \item {\tt refl} theorem, 6 |
446 \item {\tt refl} theorem, 6 |
443 \item {\tt RepFun} constant, 24, 27, 30, 32 |
447 \item {\tt RepFun} constant, 24, 27, 30, 32 |
444 \item {\tt RepFun_def} theorem, 28 |
448 \item {\tt RepFun_def} theorem, 28 |
445 \item {\tt RepFunE} theorem, 33 |
449 \item {\tt RepFunE} theorem, 33 |
446 \item {\tt RepFunI} theorem, 33 |
450 \item {\tt RepFunI} theorem, 33 |
462 \item {\tt right_inverse} theorem, 44 |
466 \item {\tt right_inverse} theorem, 44 |
463 |
467 |
464 \indexspace |
468 \indexspace |
465 |
469 |
466 \item {\tt separation} theorem, 33 |
470 \item {\tt separation} theorem, 33 |
467 \item set theory, 22--70 |
471 \item set theory, 22--71 |
468 \item {\tt Sigma} constant, 24, 27, 30, 36 |
472 \item {\tt Sigma} constant, 24, 27, 30, 36 |
469 \item {\tt Sigma_def} theorem, 29 |
473 \item {\tt Sigma_def} theorem, 29 |
470 \item {\tt SigmaE} theorem, 36 |
474 \item {\tt SigmaE} theorem, 36 |
471 \item {\tt SigmaE2} theorem, 36 |
475 \item {\tt SigmaE2} theorem, 36 |
472 \item {\tt SigmaI} theorem, 36 |
476 \item {\tt SigmaI} theorem, 36 |
486 \item {\tt step_tac}, 21 |
490 \item {\tt step_tac}, 21 |
487 \item {\tt subset_def} theorem, 28 |
491 \item {\tt subset_def} theorem, 28 |
488 \item {\tt subset_refl} theorem, 31 |
492 \item {\tt subset_refl} theorem, 31 |
489 \item {\tt subset_trans} theorem, 31 |
493 \item {\tt subset_trans} theorem, 31 |
490 \item {\tt subsetCE} theorem, 31 |
494 \item {\tt subsetCE} theorem, 31 |
491 \item {\tt subsetD} theorem, 31, 68 |
495 \item {\tt subsetD} theorem, 31, 69 |
492 \item {\tt subsetI} theorem, 31, 66, 67 |
496 \item {\tt subsetI} theorem, 31, 67, 68 |
493 \item {\tt subst} theorem, 6 |
497 \item {\tt subst} theorem, 6 |
494 \item {\tt succ} constant, 24, 30 |
498 \item {\tt succ} constant, 24, 30 |
495 \item {\tt succ_def} theorem, 29 |
499 \item {\tt succ_def} theorem, 29 |
496 \item {\tt succ_inject} theorem, 34 |
500 \item {\tt succ_inject} theorem, 34 |
497 \item {\tt succ_neq_0} theorem, 34 |
501 \item {\tt succ_neq_0} theorem, 34 |
515 \item {\tt swap_res_tac}, 14 |
519 \item {\tt swap_res_tac}, 14 |
516 \item {\tt sym} theorem, 7 |
520 \item {\tt sym} theorem, 7 |
517 |
521 |
518 \indexspace |
522 \indexspace |
519 |
523 |
|
524 \item {\tt tcset}, \bold{49} |
520 \item {\tt term} class, 3 |
525 \item {\tt term} class, 3 |
521 \item {\tt THE} symbol, 25, 27, 35 |
526 \item {\tt THE} symbol, 25, 27, 35 |
522 \item {\tt The} constant, 24, 27, 30 |
527 \item {\tt The} constant, 24, 27, 30 |
523 \item {\tt the_def} theorem, 28 |
528 \item {\tt the_def} theorem, 28 |
524 \item {\tt the_equality} theorem, 34, 35 |
529 \item {\tt the_equality} theorem, 34, 35 |
525 \item {\tt theI} theorem, 34, 35 |
530 \item {\tt theI} theorem, 34, 35 |
526 \item {\tt trace_induct}, \bold{59} |
531 \item {\tt trace_induct}, \bold{60} |
527 \item {\tt trans} theorem, 7 |
532 \item {\tt trans} theorem, 7 |
528 \item {\tt True} constant, 5 |
533 \item {\tt True} constant, 5 |
529 \item {\tt True_def} theorem, 6 |
534 \item {\tt True_def} theorem, 6 |
530 \item {\tt TrueI} theorem, 7 |
535 \item {\tt TrueI} theorem, 7 |
531 \item {\tt Trueprop} constant, 5 |
536 \item {\tt Trueprop} constant, 5 |
|
537 \item type-checking tactics, 48 |
|
538 \item {\tt type_solver_tac}, \bold{49} |
|
539 \item {\tt Typecheck_tac}, 49, \bold{49} |
|
540 \item {\tt typecheck_tac}, \bold{49} |
532 |
541 |
533 \indexspace |
542 \indexspace |
534 |
543 |
535 \item {\tt UN} symbol, 25, 27 |
544 \item {\tt UN} symbol, 25, 27 |
536 \item {\tt Un} symbol, 24 |
545 \item {\tt Un} symbol, 24 |
545 \item {\tt Un_least} theorem, 35 |
554 \item {\tt Un_least} theorem, 35 |
546 \item {\tt Un_upper1} theorem, 35 |
555 \item {\tt Un_upper1} theorem, 35 |
547 \item {\tt Un_upper2} theorem, 35 |
556 \item {\tt Un_upper2} theorem, 35 |
548 \item {\tt UnCI} theorem, 32, 34 |
557 \item {\tt UnCI} theorem, 32, 34 |
549 \item {\tt UnE} theorem, 34 |
558 \item {\tt UnE} theorem, 34 |
550 \item {\tt UnI1} theorem, 32, 34, 69 |
559 \item {\tt UnI1} theorem, 32, 34, 70 |
551 \item {\tt UnI2} theorem, 32, 34 |
560 \item {\tt UnI2} theorem, 32, 34 |
552 \item {\tt Union} constant, 24 |
561 \item {\tt Union} constant, 24 |
553 \item {\tt Union_iff} theorem, 28 |
562 \item {\tt Union_iff} theorem, 28 |
554 \item {\tt Union_least} theorem, 35 |
563 \item {\tt Union_least} theorem, 35 |
555 \item {\tt Union_Un_distrib} theorem, 40 |
564 \item {\tt Union_Un_distrib} theorem, 40 |
556 \item {\tt Union_upper} theorem, 35 |
565 \item {\tt Union_upper} theorem, 35 |
557 \item {\tt UnionE} theorem, 33, 67 |
566 \item {\tt UnionE} theorem, 33, 69 |
558 \item {\tt UnionI} theorem, 33, 67 |
567 \item {\tt UnionI} theorem, 33, 69 |
559 \item {\tt Univ} theory, 42 |
568 \item {\tt Univ} theory, 42 |
560 \item {\tt Upair} constant, 23, 24, 30 |
569 \item {\tt Upair} constant, 23, 24, 30 |
561 \item {\tt Upair_def} theorem, 28 |
570 \item {\tt Upair_def} theorem, 28 |
562 \item {\tt UpairE} theorem, 33 |
571 \item {\tt UpairE} theorem, 33 |
563 \item {\tt UpairI1} theorem, 33 |
572 \item {\tt UpairI1} theorem, 33 |