author | paulson |
Fri, 29 Oct 2004 15:16:02 +0200 | |
changeset 15270 | 8b3f707a78a7 |
parent 13639 | 8ee6ea6627e1 |
permissions | -rw-r--r-- |
1128
64b30e3cc6d4
Trancl is now based on Relation which used to be in Integ.
nipkow
parents:
diff
changeset
|
1 |
|
12905 | 2 |
(* legacy ML bindings *) |
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1842
diff
changeset
|
3 |
|
12905 | 4 |
val DomainE = thm "DomainE"; |
5 |
val DomainI = thm "DomainI"; |
|
6 |
val Domain_Collect_split = thm "Domain_Collect_split"; |
|
7 |
val Domain_Diff_subset = thm "Domain_Diff_subset"; |
|
8 |
val Domain_Id = thm "Domain_Id"; |
|
9 |
val Domain_Int_subset = thm "Domain_Int_subset"; |
|
10 |
val Domain_Un_eq = thm "Domain_Un_eq"; |
|
11 |
val Domain_Union = thm "Domain_Union"; |
|
12 |
val Domain_def = thm "Domain_def"; |
|
13 |
val Domain_diag = thm "Domain_diag"; |
|
14 |
val Domain_empty = thm "Domain_empty"; |
|
15 |
val Domain_iff = thm "Domain_iff"; |
|
16 |
val Domain_insert = thm "Domain_insert"; |
|
17 |
val Domain_mono = thm "Domain_mono"; |
|
18 |
val Field_def = thm "Field_def"; |
|
19 |
val IdE = thm "IdE"; |
|
20 |
val IdI = thm "IdI"; |
|
21 |
val Id_O_R = thm "Id_O_R"; |
|
22 |
val Id_def = thm "Id_def"; |
|
23 |
val ImageE = thm "ImageE"; |
|
24 |
val ImageI = thm "ImageI"; |
|
25 |
val Image_Collect_split = thm "Image_Collect_split"; |
|
26 |
val Image_INT_subset = thm "Image_INT_subset"; |
|
27 |
val Image_Id = thm "Image_Id"; |
|
28 |
val Image_Int_subset = thm "Image_Int_subset"; |
|
29 |
val Image_UN = thm "Image_UN"; |
|
30 |
val Image_Un = thm "Image_Un"; |
|
31 |
val Image_def = thm "Image_def"; |
|
32 |
val Image_diag = thm "Image_diag"; |
|
33 |
val Image_empty = thm "Image_empty"; |
|
34 |
val Image_eq_UN = thm "Image_eq_UN"; |
|
35 |
val Image_iff = thm "Image_iff"; |
|
36 |
val Image_mono = thm "Image_mono"; |
|
37 |
val Image_singleton = thm "Image_singleton"; |
|
38 |
val Image_singleton_iff = thm "Image_singleton_iff"; |
|
39 |
val Image_subset = thm "Image_subset"; |
|
40 |
val Image_subset_eq = thm "Image_subset_eq"; |
|
41 |
val O_assoc = thm "O_assoc"; |
|
42 |
val R_O_Id = thm "R_O_Id"; |
|
43 |
val RangeE = thm "RangeE"; |
|
44 |
val RangeI = thm "RangeI"; |
|
45 |
val Range_Collect_split = thm "Range_Collect_split"; |
|
46 |
val Range_Diff_subset = thm "Range_Diff_subset"; |
|
47 |
val Range_Id = thm "Range_Id"; |
|
48 |
val Range_Int_subset = thm "Range_Int_subset"; |
|
49 |
val Range_Un_eq = thm "Range_Un_eq"; |
|
50 |
val Range_Union = thm "Range_Union"; |
|
51 |
val Range_def = thm "Range_def"; |
|
52 |
val Range_diag = thm "Range_diag"; |
|
53 |
val Range_empty = thm "Range_empty"; |
|
54 |
val Range_iff = thm "Range_iff"; |
|
55 |
val Range_insert = thm "Range_insert"; |
|
56 |
val antisymD = thm "antisymD"; |
|
57 |
val antisymI = thm "antisymI"; |
|
58 |
val antisym_Id = thm "antisym_Id"; |
|
59 |
val antisym_converse = thm "antisym_converse"; |
|
60 |
val antisym_def = thm "antisym_def"; |
|
61 |
val converseD = thm "converseD"; |
|
62 |
val converseE = thm "converseE"; |
|
63 |
val converseI = thm "converseI"; |
|
64 |
val converse_Id = thm "converse_Id"; |
|
65 |
val converse_converse = thm "converse_converse"; |
|
66 |
val converse_def = thm "converse_def"; |
|
67 |
val converse_diag = thm "converse_diag"; |
|
68 |
val converse_iff = thm "converse_iff"; |
|
69 |
val converse_rel_comp = thm "converse_rel_comp"; |
|
70 |
val diagE = thm "diagE"; |
|
71 |
val diagI = thm "diagI"; |
|
72 |
val diag_def = thm "diag_def"; |
|
73 |
val diag_eqI = thm "diag_eqI"; |
|
74 |
val diag_iff = thm "diag_iff"; |
|
75 |
val diag_subset_Times = thm "diag_subset_Times"; |
|
76 |
val inv_image_def = thm "inv_image_def"; |
|
77 |
val pair_in_Id_conv = thm "pair_in_Id_conv"; |
|
78 |
val reflD = thm "reflD"; |
|
79 |
val reflI = thm "reflI"; |
|
80 |
val refl_converse = thm "refl_converse"; |
|
81 |
val refl_def = thm "refl_def"; |
|
82 |
val reflexive_Id = thm "reflexive_Id"; |
|
83 |
val rel_compE = thm "rel_compE"; |
|
84 |
val rel_compEpair = thm "rel_compEpair"; |
|
85 |
val rel_compI = thm "rel_compI"; |
|
86 |
val rel_comp_def = thm "rel_comp_def"; |
|
87 |
val rel_comp_mono = thm "rel_comp_mono"; |
|
88 |
val rel_comp_subset_Sigma = thm "rel_comp_subset_Sigma"; |
|
89 |
val rev_ImageI = thm "rev_ImageI"; |
|
90 |
val single_valuedD = thm "single_valuedD"; |
|
91 |
val single_valuedI = thm "single_valuedI"; |
|
92 |
val single_valued_def = thm "single_valued_def"; |
|
93 |
val sym_def = thm "sym_def"; |
|
94 |
val transD = thm "transD"; |
|
95 |
val transI = thm "transI"; |
|
96 |
val trans_Id = thm "trans_Id"; |
|
97 |
val trans_O_subset = thm "trans_O_subset"; |
|
98 |
val trans_converse = thm "trans_converse"; |
|
99 |
val trans_def = thm "trans_def"; |
|
100 |
val trans_inv_image = thm "trans_inv_image"; |