| author | paulson |
| Mon, 05 May 2003 18:34:16 +0200 | |
| changeset 13960 | 70f9158b6695 |
| parent 13482 | 2bb7200a99cf |
| permissions | -rw-r--r-- |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
1 |
|
| 13482 | 2 |
(* legacy ML bindings *) |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
3 |
|
| 13482 | 4 |
val UN_UN_split_split_eq = thm "UN_UN_split_split_eq"; |
5 |
val UN_constant_eq = thm "UN_constant_eq"; |
|
6 |
val UN_equiv_class = thm "UN_equiv_class"; |
|
7 |
val UN_equiv_class2 = thm "UN_equiv_class2"; |
|
8 |
val UN_equiv_class_inject = thm "UN_equiv_class_inject"; |
|
9 |
val UN_equiv_class_type = thm "UN_equiv_class_type"; |
|
10 |
val UN_equiv_class_type2 = thm "UN_equiv_class_type2"; |
|
11 |
val Union_quotient = thm "Union_quotient"; |
|
12 |
val comp_equivI = thm "comp_equivI"; |
|
13 |
val congruent2I = thm "congruent2I"; |
|
14 |
val congruent2_commuteI = thm "congruent2_commuteI"; |
|
15 |
val congruent2_def = thm "congruent2_def"; |
|
16 |
val congruent2_implies_congruent = thm "congruent2_implies_congruent"; |
|
17 |
val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN"; |
|
18 |
val congruent_def = thm "congruent_def"; |
|
19 |
val eq_equiv_class = thm "eq_equiv_class"; |
|
20 |
val eq_equiv_class_iff = thm "eq_equiv_class_iff"; |
|
21 |
val equiv_class_eq = thm "equiv_class_eq"; |
|
22 |
val equiv_class_eq_iff = thm "equiv_class_eq_iff"; |
|
23 |
val equiv_class_nondisjoint = thm "equiv_class_nondisjoint"; |
|
24 |
val equiv_class_self = thm "equiv_class_self"; |
|
25 |
val equiv_class_subset = thm "equiv_class_subset"; |
|
26 |
val equiv_comp_eq = thm "equiv_comp_eq"; |
|
27 |
val equiv_def = thm "equiv_def"; |
|
28 |
val equiv_imp_dvd_card = thm "equiv_imp_dvd_card"; |
|
29 |
val equiv_type = thm "equiv_type"; |
|
30 |
val finite_equiv_class = thm "finite_equiv_class"; |
|
31 |
val finite_quotient = thm "finite_quotient"; |
|
32 |
val quotientE = thm "quotientE"; |
|
33 |
val quotientI = thm "quotientI"; |
|
34 |
val quotient_def = thm "quotient_def"; |
|
35 |
val quotient_disj = thm "quotient_disj"; |
|
36 |
val refl_comp_subset = thm "refl_comp_subset"; |
|
37 |
val subset_equiv_class = thm "subset_equiv_class"; |
|
38 |
val sym_trans_comp_subset = thm "sym_trans_comp_subset"; |