src/HOL/Set.ML
changeset 21669 c68717c16013
parent 21668 2d811ae6752a
child 21670 704510b508ef
     1.1 --- a/src/HOL/Set.ML	Tue Dec 05 22:14:53 2006 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,433 +0,0 @@
     1.4 -
     1.5 -(* legacy ML bindings *)
     1.6 -
     1.7 -val Ball_def = thm "Ball_def";
     1.8 -val Bex_def = thm "Bex_def";
     1.9 -val CollectD = thm "CollectD";
    1.10 -val CollectE = thm "CollectE";
    1.11 -val CollectI = thm "CollectI";
    1.12 -val Collect_all_eq = thm "Collect_all_eq";
    1.13 -val Collect_ball_eq = thm "Collect_ball_eq";
    1.14 -val Collect_bex_eq = thm "Collect_bex_eq";
    1.15 -val Collect_cong = thm "Collect_cong";
    1.16 -val Collect_conj_eq = thm "Collect_conj_eq";
    1.17 -val Collect_const = thm "Collect_const";
    1.18 -val Collect_disj_eq = thm "Collect_disj_eq";
    1.19 -val Collect_empty_eq = thm "Collect_empty_eq";
    1.20 -val Collect_ex_eq = thm "Collect_ex_eq";
    1.21 -val Collect_mem_eq = thm "Collect_mem_eq";
    1.22 -val Collect_mono = thm "Collect_mono";
    1.23 -val Collect_neg_eq = thm "Collect_neg_eq";
    1.24 -val ComplD = thm "ComplD";
    1.25 -val ComplE = thm "ComplE";
    1.26 -val ComplI = thm "ComplI";
    1.27 -val Compl_Diff_eq = thm "Compl_Diff_eq";
    1.28 -val Compl_INT = thm "Compl_INT";
    1.29 -val Compl_Int = thm "Compl_Int";
    1.30 -val Compl_UN = thm "Compl_UN";
    1.31 -val Compl_UNIV_eq = thm "Compl_UNIV_eq";
    1.32 -val Compl_Un = thm "Compl_Un";
    1.33 -val Compl_anti_mono = thm "Compl_anti_mono";
    1.34 -val Compl_def = thm "Compl_def";
    1.35 -val Compl_disjoint = thm "Compl_disjoint";
    1.36 -val Compl_disjoint2 = thm "Compl_disjoint2";
    1.37 -val Compl_empty_eq = thm "Compl_empty_eq";
    1.38 -val Compl_eq_Compl_iff = thm "Compl_eq_Compl_iff";
    1.39 -val Compl_iff = thm "Compl_iff";
    1.40 -val Compl_partition = thm "Compl_partition";
    1.41 -val Compl_subset_Compl_iff = thm "Compl_subset_Compl_iff";
    1.42 -val DiffD1 = thm "DiffD1";
    1.43 -val DiffD2 = thm "DiffD2";
    1.44 -val DiffE = thm "DiffE";
    1.45 -val DiffI = thm "DiffI";
    1.46 -val Diff_Compl = thm "Diff_Compl";
    1.47 -val Diff_Int = thm "Diff_Int";
    1.48 -val Diff_Int_distrib = thm "Diff_Int_distrib";
    1.49 -val Diff_Int_distrib2 = thm "Diff_Int_distrib2";
    1.50 -val Diff_UNIV = thm "Diff_UNIV";
    1.51 -val Diff_Un = thm "Diff_Un";
    1.52 -val Diff_cancel = thm "Diff_cancel";
    1.53 -val Diff_disjoint = thm "Diff_disjoint";
    1.54 -val Diff_empty = thm "Diff_empty";
    1.55 -val Diff_eq = thm "Diff_eq";
    1.56 -val Diff_eq_empty_iff = thm "Diff_eq_empty_iff";
    1.57 -val Diff_iff = thm "Diff_iff";
    1.58 -val Diff_insert = thm "Diff_insert";
    1.59 -val Diff_insert0 = thm "Diff_insert0";
    1.60 -val Diff_insert2 = thm "Diff_insert2";
    1.61 -val Diff_insert_absorb = thm "Diff_insert_absorb";
    1.62 -val Diff_mono = thm "Diff_mono";
    1.63 -val Diff_partition = thm "Diff_partition";
    1.64 -val Diff_subset = thm "Diff_subset";
    1.65 -val Diff_triv = thm "Diff_triv";
    1.66 -val INTER_def = thm "INTER_def";
    1.67 -val INT_D = thm "INT_D";
    1.68 -val INT_E = thm "INT_E";
    1.69 -val INT_I = thm "INT_I";
    1.70 -val INT_Int_distrib = thm "INT_Int_distrib";
    1.71 -val INT_Un = thm "INT_Un";
    1.72 -val INT_absorb = thm "INT_absorb";
    1.73 -val INT_anti_mono = thm "INT_anti_mono";
    1.74 -val INT_bool_eq = thm "INT_bool_eq";
    1.75 -val INT_cong = thm "INT_cong";
    1.76 -val INT_constant = thm "INT_constant";
    1.77 -val INT_empty = thm "INT_empty";
    1.78 -val INT_eq = thm "INT_eq";
    1.79 -val INT_greatest = thm "INT_greatest";
    1.80 -val INT_iff = thm "INT_iff";
    1.81 -val INT_insert = thm "INT_insert";
    1.82 -val INT_insert_distrib = thm "INT_insert_distrib";
    1.83 -val INT_lower = thm "INT_lower";
    1.84 -val INT_simps = thms "INT_simps";
    1.85 -val INT_subset_iff = thm "INT_subset_iff";
    1.86 -val IntD1 = thm "IntD1";
    1.87 -val IntD2 = thm "IntD2";
    1.88 -val IntE = thm "IntE";
    1.89 -val IntI = thm "IntI";
    1.90 -val Int_Collect = thm "Int_Collect";
    1.91 -val Int_Collect_mono = thm "Int_Collect_mono";
    1.92 -val Int_Diff = thm "Int_Diff";
    1.93 -val Int_Inter_image = thm "Int_Inter_image";
    1.94 -val Int_UNIV = thm "Int_UNIV";
    1.95 -val Int_UNIV_left = thm "Int_UNIV_left";
    1.96 -val Int_UNIV_right = thm "Int_UNIV_right";
    1.97 -val Int_UN_distrib = thm "Int_UN_distrib";
    1.98 -val Int_UN_distrib2 = thm "Int_UN_distrib2";
    1.99 -val Int_Un_distrib = thm "Int_Un_distrib";
   1.100 -val Int_Un_distrib2 = thm "Int_Un_distrib2";
   1.101 -val Int_Union = thm "Int_Union";
   1.102 -val Int_Union2 = thm "Int_Union2";
   1.103 -val Int_absorb = thm "Int_absorb";
   1.104 -val Int_absorb1 = thm "Int_absorb1";
   1.105 -val Int_absorb2 = thm "Int_absorb2";
   1.106 -val Int_ac = thms "Int_ac";
   1.107 -val Int_assoc = thm "Int_assoc";
   1.108 -val Int_commute = thm "Int_commute";
   1.109 -val Int_def = thm "Int_def";
   1.110 -val Int_empty_left = thm "Int_empty_left";
   1.111 -val Int_empty_right = thm "Int_empty_right";
   1.112 -val Int_eq_Inter = thm "Int_eq_Inter";
   1.113 -val Int_greatest = thm "Int_greatest";
   1.114 -val Int_iff = thm "Int_iff";
   1.115 -val Int_insert_left = thm "Int_insert_left";
   1.116 -val Int_insert_right = thm "Int_insert_right";
   1.117 -val Int_left_absorb = thm "Int_left_absorb";
   1.118 -val Int_left_commute = thm "Int_left_commute";
   1.119 -val Int_lower1 = thm "Int_lower1";
   1.120 -val Int_lower2 = thm "Int_lower2";
   1.121 -val Int_mono = thm "Int_mono";
   1.122 -val Int_subset_iff = thm "Int_subset_iff";
   1.123 -val InterD = thm "InterD";
   1.124 -val InterE = thm "InterE";
   1.125 -val InterI = thm "InterI";
   1.126 -val Inter_UNIV = thm "Inter_UNIV";
   1.127 -val Inter_Un_distrib = thm "Inter_Un_distrib";
   1.128 -val Inter_Un_subset = thm "Inter_Un_subset";
   1.129 -val Inter_anti_mono = thm "Inter_anti_mono";
   1.130 -val Inter_def = thm "Inter_def";
   1.131 -val Inter_empty = thm "Inter_empty";
   1.132 -val Inter_greatest = thm "Inter_greatest";
   1.133 -val Inter_iff = thm "Inter_iff";
   1.134 -val Inter_image_eq = thm "Inter_image_eq";
   1.135 -val Inter_insert = thm "Inter_insert";
   1.136 -val Inter_lower = thm "Inter_lower";
   1.137 -val PowD = thm "PowD";
   1.138 -val PowI = thm "PowI";
   1.139 -val Pow_Compl = thm "Pow_Compl";
   1.140 -val Pow_INT_eq = thm "Pow_INT_eq";
   1.141 -val Pow_Int_eq = thm "Pow_Int_eq";
   1.142 -val Pow_UNIV = thm "Pow_UNIV";
   1.143 -val Pow_bottom = thm "Pow_bottom";
   1.144 -val Pow_def = thm "Pow_def";
   1.145 -val Pow_empty = thm "Pow_empty";
   1.146 -val Pow_iff = thm "Pow_iff";
   1.147 -val Pow_insert = thm "Pow_insert";
   1.148 -val Pow_mono = thm "Pow_mono";
   1.149 -val Pow_top = thm "Pow_top";
   1.150 -val UNION_def = thm "UNION_def";
   1.151 -val UNIV_I = thm "UNIV_I";
   1.152 -val UNIV_def = thm "UNIV_def";
   1.153 -val UNIV_not_empty = thm "UNIV_not_empty";
   1.154 -val UNIV_witness = thm "UNIV_witness";
   1.155 -val UN_E = thm "UN_E";
   1.156 -val UN_I = thm "UN_I";
   1.157 -val UN_Pow_subset = thm "UN_Pow_subset";
   1.158 -val UN_UN_flatten = thm "UN_UN_flatten";
   1.159 -val UN_Un = thm "UN_Un";
   1.160 -val UN_Un_distrib = thm "UN_Un_distrib";
   1.161 -val UN_absorb = thm "UN_absorb";
   1.162 -val UN_bool_eq = thm "UN_bool_eq";
   1.163 -val UN_cong = thm "UN_cong";
   1.164 -val UN_constant = thm "UN_constant";
   1.165 -val UN_empty = thm "UN_empty";
   1.166 -val UN_empty2 = thm "UN_empty2";
   1.167 -val UN_eq = thm "UN_eq";
   1.168 -val UN_iff = thm "UN_iff";
   1.169 -val UN_insert = thm "UN_insert";
   1.170 -val UN_insert_distrib = thm "UN_insert_distrib";
   1.171 -val UN_least = thm "UN_least";
   1.172 -val UN_mono = thm "UN_mono";
   1.173 -val UN_simps = thms "UN_simps";
   1.174 -val UN_singleton = thm "UN_singleton";
   1.175 -val UN_subset_iff = thm "UN_subset_iff";
   1.176 -val UN_upper = thm "UN_upper";
   1.177 -val UnCI = thm "UnCI";
   1.178 -val UnE = thm "UnE";
   1.179 -val UnI1 = thm "UnI1";
   1.180 -val UnI2 = thm "UnI2";
   1.181 -val Un_Diff = thm "Un_Diff";
   1.182 -val Un_Diff_Int = thm "Un_Diff_Int";
   1.183 -val Un_Diff_cancel = thm "Un_Diff_cancel";
   1.184 -val Un_Diff_cancel2 = thm "Un_Diff_cancel2";
   1.185 -val Un_INT_distrib = thm "Un_INT_distrib";
   1.186 -val Un_INT_distrib2 = thm "Un_INT_distrib2";
   1.187 -val Un_Int_assoc_eq = thm "Un_Int_assoc_eq";
   1.188 -val Un_Int_crazy = thm "Un_Int_crazy";
   1.189 -val Un_Int_distrib = thm "Un_Int_distrib";
   1.190 -val Un_Int_distrib2 = thm "Un_Int_distrib2";
   1.191 -val Un_Inter = thm "Un_Inter";
   1.192 -val Un_Pow_subset = thm "Un_Pow_subset";
   1.193 -val Un_UNIV_left = thm "Un_UNIV_left";
   1.194 -val Un_UNIV_right = thm "Un_UNIV_right";
   1.195 -val Un_Union_image = thm "Un_Union_image";
   1.196 -val Un_absorb = thm "Un_absorb";
   1.197 -val Un_absorb1 = thm "Un_absorb1";
   1.198 -val Un_absorb2 = thm "Un_absorb2";
   1.199 -val Un_ac = thms "Un_ac";
   1.200 -val Un_assoc = thm "Un_assoc";
   1.201 -val Un_commute = thm "Un_commute";
   1.202 -val Un_def = thm "Un_def";
   1.203 -val Un_empty = thm "Un_empty";
   1.204 -val Un_empty_left = thm "Un_empty_left";
   1.205 -val Un_empty_right = thm "Un_empty_right";
   1.206 -val Un_eq_UN = thm "Un_eq_UN";
   1.207 -val Un_eq_Union = thm "Un_eq_Union";
   1.208 -val Un_iff = thm "Un_iff";
   1.209 -val Un_insert_left = thm "Un_insert_left";
   1.210 -val Un_insert_right = thm "Un_insert_right";
   1.211 -val Un_least = thm "Un_least";
   1.212 -val Un_left_absorb = thm "Un_left_absorb";
   1.213 -val Un_left_commute = thm "Un_left_commute";
   1.214 -val Un_mono = thm "Un_mono";
   1.215 -val Un_subset_iff = thm "Un_subset_iff";
   1.216 -val Un_upper1 = thm "Un_upper1";
   1.217 -val Un_upper2 = thm "Un_upper2";
   1.218 -val UnionE = thm "UnionE";
   1.219 -val UnionI = thm "UnionI";
   1.220 -val Union_Int_subset = thm "Union_Int_subset";
   1.221 -val Union_Pow_eq = thm "Union_Pow_eq";
   1.222 -val Union_UNIV = thm "Union_UNIV";
   1.223 -val Union_Un_distrib = thm "Union_Un_distrib";
   1.224 -val Union_def = thm "Union_def";
   1.225 -val Union_disjoint = thm "Union_disjoint";
   1.226 -val Union_empty = thm "Union_empty";
   1.227 -val Union_empty_conv = thm "Union_empty_conv";
   1.228 -val Union_iff = thm "Union_iff";
   1.229 -val Union_image_eq = thm "Union_image_eq";
   1.230 -val Union_insert = thm "Union_insert";
   1.231 -val Union_least = thm "Union_least";
   1.232 -val Union_mono = thm "Union_mono";
   1.233 -val Union_upper = thm "Union_upper";
   1.234 -val all_bool_eq = thm "all_bool_eq";
   1.235 -val all_mono = thm "all_mono";
   1.236 -val all_not_in_conv = thm "all_not_in_conv";
   1.237 -val atomize_ball = thm "atomize_ball";
   1.238 -val ballE = thm "ballE";
   1.239 -val ballI = thm "ballI";
   1.240 -val ball_UN = thm "ball_UN";
   1.241 -val ball_UNIV = thm "ball_UNIV";
   1.242 -val ball_Un = thm "ball_Un";
   1.243 -val ball_cong = thm "ball_cong";
   1.244 -val ball_conj_distrib = thm "ball_conj_distrib";
   1.245 -val ball_empty = thm "ball_empty";
   1.246 -val ball_one_point1 = thm "ball_one_point1";
   1.247 -val ball_one_point2 = thm "ball_one_point2";
   1.248 -val ball_simps = thms "ball_simps";
   1.249 -val ball_triv = thm "ball_triv";
   1.250 -val basic_monos = thms "basic_monos";
   1.251 -val bexCI = thm "bexCI";
   1.252 -val bexE = thm "bexE";
   1.253 -val bexI = thm "bexI";
   1.254 -val bex_UN = thm "bex_UN";
   1.255 -val bex_UNIV = thm "bex_UNIV";
   1.256 -val bex_Un = thm "bex_Un";
   1.257 -val bex_cong = thm "bex_cong";
   1.258 -val bex_disj_distrib = thm "bex_disj_distrib";
   1.259 -val bex_empty = thm "bex_empty";
   1.260 -val bex_one_point1 = thm "bex_one_point1";
   1.261 -val bex_one_point2 = thm "bex_one_point2";
   1.262 -val bex_simps = thms "bex_simps";
   1.263 -val bex_triv = thm "bex_triv";
   1.264 -val bex_triv_one_point1 = thm "bex_triv_one_point1";
   1.265 -val bex_triv_one_point2 = thm "bex_triv_one_point2";
   1.266 -val bool_induct = thm "bool_induct";
   1.267 -val bspec = thm "bspec";
   1.268 -val conj_mono = thm "conj_mono";
   1.269 -val contra_subsetD = thm "contra_subsetD";
   1.270 -val diff_single_insert = thm "diff_single_insert";
   1.271 -val disj_mono = thm "disj_mono";
   1.272 -val disjoint_eq_subset_Compl = thm "disjoint_eq_subset_Compl";
   1.273 -val disjoint_iff_not_equal = thm "disjoint_iff_not_equal";
   1.274 -val distinct_lemma = thm "distinct_lemma";
   1.275 -val double_complement = thm "double_complement";
   1.276 -val double_diff = thm "double_diff";
   1.277 -val emptyE = thm "emptyE";
   1.278 -val empty_Diff = thm "empty_Diff";
   1.279 -val empty_def = thm "empty_def";
   1.280 -val empty_iff = thm "empty_iff";
   1.281 -val empty_subsetI = thm "empty_subsetI";
   1.282 -val eq_to_mono = thm "eq_to_mono";
   1.283 -val eq_to_mono2 = thm "eq_to_mono2";
   1.284 -val eqset_imp_iff = thm "eqset_imp_iff";
   1.285 -val equalityCE = thm "equalityCE";
   1.286 -val equalityD1 = thm "equalityD1";
   1.287 -val equalityD2 = thm "equalityD2";
   1.288 -val equalityE = thm "equalityE";
   1.289 -val equalityI = thm "equalityI";
   1.290 -val equals0D = thm "equals0D";
   1.291 -val equals0I = thm "equals0I";
   1.292 -val ex_bool_eq = thm "ex_bool_eq";
   1.293 -val ex_mono = thm "ex_mono";
   1.294 -val full_SetCompr_eq = thm "full_SetCompr_eq";
   1.295 -val if_image_distrib = thm "if_image_distrib";
   1.296 -val imageE = thm "imageE";
   1.297 -val imageI = thm "imageI";
   1.298 -val image_Collect = thm "image_Collect";
   1.299 -val image_Un = thm "image_Un";
   1.300 -val image_Union = thm "image_Union";
   1.301 -val image_cong = thm "image_cong";
   1.302 -val image_constant = thm "image_constant";
   1.303 -val image_def = thm "image_def";
   1.304 -val image_empty = thm "image_empty";
   1.305 -val image_eqI = thm "image_eqI";
   1.306 -val image_iff = thm "image_iff";
   1.307 -val image_image = thm "image_image";
   1.308 -val image_insert = thm "image_insert";
   1.309 -val image_is_empty = thm "image_is_empty";
   1.310 -val image_mono = thm "image_mono";
   1.311 -val image_subsetI = thm "image_subsetI";
   1.312 -val image_subset_iff = thm "image_subset_iff";
   1.313 -val imp_mono = thm "imp_mono";
   1.314 -val imp_refl = thm "imp_refl";
   1.315 -val in_mono = thm "in_mono";
   1.316 -val insertCI = thm "insertCI";
   1.317 -val insertE = thm "insertE";
   1.318 -val insertI1 = thm "insertI1";
   1.319 -val insertI2 = thm "insertI2";
   1.320 -val insert_Collect = thm "insert_Collect";
   1.321 -val insert_Diff = thm "insert_Diff";
   1.322 -val insert_Diff1 = thm "insert_Diff1";
   1.323 -val insert_Diff_if = thm "insert_Diff_if";
   1.324 -val insert_absorb = thm "insert_absorb";
   1.325 -val insert_absorb2 = thm "insert_absorb2";
   1.326 -val insert_commute = thm "insert_commute";
   1.327 -val insert_def = thm "insert_def";
   1.328 -val insert_iff = thm "insert_iff";
   1.329 -val insert_image = thm "insert_image";
   1.330 -val insert_is_Un = thm "insert_is_Un";
   1.331 -val insert_mono = thm "insert_mono";
   1.332 -val insert_not_empty = thm "insert_not_empty";
   1.333 -val insert_subset = thm "insert_subset";
   1.334 -val mem_Collect_eq = thm "mem_Collect_eq";
   1.335 -val mem_simps = thms "mem_simps";
   1.336 -val mk_disjoint_insert = thm "mk_disjoint_insert";
   1.337 -val mono_Int = thm "mono_Int";
   1.338 -val mono_Un = thm "mono_Un";
   1.339 -val not_psubset_empty = thm "not_psubset_empty";
   1.340 -val psubsetI = thm "psubsetI";
   1.341 -val psubset_def = thm "psubset_def";
   1.342 -val psubset_eq = thm "psubset_eq";
   1.343 -val psubset_imp_ex_mem = thm "psubset_imp_ex_mem";
   1.344 -val psubset_imp_subset = thm "psubset_imp_subset";
   1.345 -val psubset_insert_iff = thm "psubset_insert_iff";
   1.346 -val psubset_subset_trans = thm "psubset_subset_trans";
   1.347 -val rangeE = thm "rangeE";
   1.348 -val rangeI = thm "rangeI";
   1.349 -val range_composition = thm "range_composition";
   1.350 -val range_eqI = thm "range_eqI";
   1.351 -val rev_bexI = thm "rev_bexI";
   1.352 -val rev_image_eqI = thm "rev_image_eqI";
   1.353 -val rev_subsetD = thm "rev_subsetD";
   1.354 -val set_diff_def = thm "set_diff_def";
   1.355 -val set_eq_subset = thm "set_eq_subset";
   1.356 -val set_ext = thm "set_ext";
   1.357 -val singletonD = thm "singletonD";
   1.358 -val singletonE = thm "singletonE";
   1.359 -val singletonI = thm "singletonI";
   1.360 -val singleton_conv = thm "singleton_conv";
   1.361 -val singleton_conv2 = thm "singleton_conv2";
   1.362 -val singleton_iff = thm "singleton_iff";
   1.363 -val singleton_inject = thm "singleton_inject";
   1.364 -val singleton_insert_inj_eq = thm "singleton_insert_inj_eq";
   1.365 -val singleton_insert_inj_eq' = thm "singleton_insert_inj_eq'";
   1.366 -val split_if_eq1 = thm "split_if_eq1";
   1.367 -val split_if_eq2 = thm "split_if_eq2";
   1.368 -val split_if_mem1 = thm "split_if_mem1";
   1.369 -val split_if_mem2 = thm "split_if_mem2";
   1.370 -val split_ifs = thms "split_ifs";
   1.371 -val strip = thms "strip";
   1.372 -val subsetCE = thm "subsetCE";
   1.373 -val subsetD = thm "subsetD";
   1.374 -val subsetI = thm "subsetI";
   1.375 -val subset_Compl_self_eq = thm "subset_Compl_self_eq";
   1.376 -val subset_Pow_Union = thm "subset_Pow_Union";
   1.377 -val subset_UNIV = thm "subset_UNIV";
   1.378 -val subset_Un_eq = thm "subset_Un_eq";
   1.379 -val subset_antisym = thm "subset_antisym";
   1.380 -val subset_def = thm "subset_def";
   1.381 -val subset_empty = thm "subset_empty";
   1.382 -val subset_iff = thm "subset_iff";
   1.383 -val subset_iff_psubset_eq = thm "subset_iff_psubset_eq";
   1.384 -val subset_image_iff = thm "subset_image_iff";
   1.385 -val subset_insert = thm "subset_insert";
   1.386 -val subset_insertI = thm "subset_insertI";
   1.387 -val subset_insert_iff = thm "subset_insert_iff";
   1.388 -val subset_psubset_trans = thm "subset_psubset_trans";
   1.389 -val subset_refl = thm "subset_refl";
   1.390 -val subset_singletonD = thm "subset_singletonD";
   1.391 -val subset_trans = thm "subset_trans";
   1.392 -val vimageD = thm "vimageD";
   1.393 -val vimageE = thm "vimageE";
   1.394 -val vimageI = thm "vimageI";
   1.395 -val vimageI2 = thm "vimageI2";
   1.396 -val vimage_Collect = thm "vimage_Collect";
   1.397 -val vimage_Collect_eq = thm "vimage_Collect_eq";
   1.398 -val vimage_Compl = thm "vimage_Compl";
   1.399 -val vimage_Diff = thm "vimage_Diff";
   1.400 -val vimage_INT = thm "vimage_INT";
   1.401 -val vimage_Int = thm "vimage_Int";
   1.402 -val vimage_UN = thm "vimage_UN";
   1.403 -val vimage_UNIV = thm "vimage_UNIV";
   1.404 -val vimage_Un = thm "vimage_Un";
   1.405 -val vimage_Union = thm "vimage_Union";
   1.406 -val vimage_def = thm "vimage_def";
   1.407 -val vimage_empty = thm "vimage_empty";
   1.408 -val vimage_eq = thm "vimage_eq";
   1.409 -val vimage_eq_UN = thm "vimage_eq_UN";
   1.410 -val vimage_insert = thm "vimage_insert";
   1.411 -val vimage_mono = thm "vimage_mono";
   1.412 -val vimage_singleton_eq = thm "vimage_singleton_eq";
   1.413 -
   1.414 -structure Set =
   1.415 -struct
   1.416 -  val thy = the_context ();
   1.417 -  val Ball_def = Ball_def;
   1.418 -  val Bex_def = Bex_def;
   1.419 -  val Collect_mem_eq = Collect_mem_eq;
   1.420 -  val Compl_def = Compl_def;
   1.421 -  val INTER_def = INTER_def;
   1.422 -  val Int_def = Int_def;
   1.423 -  val Inter_def = Inter_def;
   1.424 -  val Pow_def = Pow_def;
   1.425 -  val UNION_def = UNION_def;
   1.426 -  val UNIV_def = UNIV_def;
   1.427 -  val Un_def = Un_def;
   1.428 -  val Union_def = Union_def;
   1.429 -  val empty_def = empty_def;
   1.430 -  val image_def = image_def;
   1.431 -  val insert_def = insert_def;
   1.432 -  val mem_Collect_eq = mem_Collect_eq;
   1.433 -  val psubset_def = psubset_def;
   1.434 -  val set_diff_def = set_diff_def;
   1.435 -  val subset_def = subset_def;
   1.436 -end;