22 val mem_Collect_eq = mem_Collect_eq; |
22 val mem_Collect_eq = mem_Collect_eq; |
23 val psubset_def = psubset_def; |
23 val psubset_def = psubset_def; |
24 val set_diff_def = set_diff_def; |
24 val set_diff_def = set_diff_def; |
25 val subset_def = subset_def; |
25 val subset_def = subset_def; |
26 end; |
26 end; |
|
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"; |