|
923
|
1 |
|
|
11979
|
2 |
(* legacy ML bindings *)
|
|
923
|
3 |
|
|
11979
|
4 |
structure Set =
|
|
|
5 |
struct
|
|
|
6 |
val thy = the_context ();
|
|
|
7 |
val Ball_def = Ball_def;
|
|
|
8 |
val Bex_def = Bex_def;
|
|
|
9 |
val Collect_mem_eq = Collect_mem_eq;
|
|
|
10 |
val Compl_def = Compl_def;
|
|
|
11 |
val INTER_def = INTER_def;
|
|
|
12 |
val Int_def = Int_def;
|
|
|
13 |
val Inter_def = Inter_def;
|
|
|
14 |
val Pow_def = Pow_def;
|
|
|
15 |
val UNION_def = UNION_def;
|
|
|
16 |
val UNIV_def = UNIV_def;
|
|
|
17 |
val Un_def = Un_def;
|
|
|
18 |
val Union_def = Union_def;
|
|
|
19 |
val empty_def = empty_def;
|
|
|
20 |
val image_def = image_def;
|
|
|
21 |
val insert_def = insert_def;
|
|
|
22 |
val mem_Collect_eq = mem_Collect_eq;
|
|
|
23 |
val psubset_def = psubset_def;
|
|
|
24 |
val set_diff_def = set_diff_def;
|
|
|
25 |
val subset_def = subset_def;
|
|
|
26 |
end;
|
|
12257
|
27 |
|
|
|
28 |
val vimageD = thm "vimageD";
|
|
|
29 |
val vimageE = thm "vimageE";
|
|
|
30 |
val vimageI = thm "vimageI";
|
|
|
31 |
val vimageI2 = thm "vimageI2";
|
|
|
32 |
val vimage_Collect = thm "vimage_Collect";
|
|
|
33 |
val vimage_Collect_eq = thm "vimage_Collect_eq";
|
|
|
34 |
val vimage_Compl = thm "vimage_Compl";
|
|
|
35 |
val vimage_Diff = thm "vimage_Diff";
|
|
|
36 |
val vimage_INT = thm "vimage_INT";
|
|
|
37 |
val vimage_Int = thm "vimage_Int";
|
|
|
38 |
val vimage_UN = thm "vimage_UN";
|
|
|
39 |
val vimage_UNIV = thm "vimage_UNIV";
|
|
|
40 |
val vimage_Un = thm "vimage_Un";
|
|
|
41 |
val vimage_Union = thm "vimage_Union";
|
|
|
42 |
val vimage_def = thm "vimage_def";
|
|
|
43 |
val vimage_empty = thm "vimage_empty";
|
|
|
44 |
val vimage_eq = thm "vimage_eq";
|
|
|
45 |
val vimage_eq_UN = thm "vimage_eq_UN";
|
|
|
46 |
val vimage_insert = thm "vimage_insert";
|
|
|
47 |
val vimage_mono = thm "vimage_mono";
|
|
|
48 |
val vimage_singleton_eq = thm "vimage_singleton_eq";
|