|
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;
|