(* legacy ML bindings *) val Ball_def = thm "Ball_def"; val Bex_def = thm "Bex_def"; val CollectD = thm "CollectD"; val CollectE = thm "CollectE"; val CollectI = thm "CollectI"; val Collect_all_eq = thm "Collect_all_eq"; val Collect_ball_eq = thm "Collect_ball_eq"; val Collect_bex_eq = thm "Collect_bex_eq"; val Collect_cong = thm "Collect_cong"; val Collect_conj_eq = thm "Collect_conj_eq"; val Collect_const = thm "Collect_const"; val Collect_disj_eq = thm "Collect_disj_eq"; val Collect_empty_eq = thm "Collect_empty_eq"; val Collect_ex_eq = thm "Collect_ex_eq"; val Collect_mem_eq = thm "Collect_mem_eq"; val Collect_mono = thm "Collect_mono"; val Collect_neg_eq = thm "Collect_neg_eq"; val ComplD = thm "ComplD"; val ComplE = thm "ComplE"; val ComplI = thm "ComplI"; val Compl_Diff_eq = thm "Compl_Diff_eq"; val Compl_INT = thm "Compl_INT"; val Compl_Int = thm "Compl_Int"; val Compl_UN = thm "Compl_UN"; val Compl_UNIV_eq = thm "Compl_UNIV_eq"; val Compl_Un = thm "Compl_Un"; val Compl_anti_mono = thm "Compl_anti_mono"; val Compl_def = thm "Compl_def"; val Compl_disjoint = thm "Compl_disjoint"; val Compl_disjoint2 = thm "Compl_disjoint2"; val Compl_empty_eq = thm "Compl_empty_eq"; val Compl_eq_Compl_iff = thm "Compl_eq_Compl_iff"; val Compl_iff = thm "Compl_iff"; val Compl_partition = thm "Compl_partition"; val Compl_subset_Compl_iff = thm "Compl_subset_Compl_iff"; val DiffD1 = thm "DiffD1"; val DiffD2 = thm "DiffD2"; val DiffE = thm "DiffE"; val DiffI = thm "DiffI"; val Diff_Compl = thm "Diff_Compl"; val Diff_Int = thm "Diff_Int"; val Diff_Int_distrib = thm "Diff_Int_distrib"; val Diff_Int_distrib2 = thm "Diff_Int_distrib2"; val Diff_UNIV = thm "Diff_UNIV"; val Diff_Un = thm "Diff_Un"; val Diff_cancel = thm "Diff_cancel"; val Diff_disjoint = thm "Diff_disjoint"; val Diff_empty = thm "Diff_empty"; val Diff_eq = thm "Diff_eq"; val Diff_eq_empty_iff = thm "Diff_eq_empty_iff"; val Diff_iff = thm "Diff_iff"; val Diff_insert = thm "Diff_insert"; val Diff_insert0 = thm "Diff_insert0"; val Diff_insert2 = thm "Diff_insert2"; val Diff_insert_absorb = thm "Diff_insert_absorb"; val Diff_mono = thm "Diff_mono"; val Diff_partition = thm "Diff_partition"; val Diff_subset = thm "Diff_subset"; val Diff_triv = thm "Diff_triv"; val INTER_def = thm "INTER_def"; val INT_D = thm "INT_D"; val INT_E = thm "INT_E"; val INT_I = thm "INT_I"; val INT_Int_distrib = thm "INT_Int_distrib"; val INT_Un = thm "INT_Un"; val INT_absorb = thm "INT_absorb"; val INT_anti_mono = thm "INT_anti_mono"; val INT_bool_eq = thm "INT_bool_eq"; val INT_cong = thm "INT_cong"; val INT_constant = thm "INT_constant"; val INT_empty = thm "INT_empty"; val INT_eq = thm "INT_eq"; val INT_greatest = thm "INT_greatest"; val INT_iff = thm "INT_iff"; val INT_insert = thm "INT_insert"; val INT_insert_distrib = thm "INT_insert_distrib"; val INT_lower = thm "INT_lower"; val INT_simps = thms "INT_simps"; val INT_subset_iff = thm "INT_subset_iff"; val IntD1 = thm "IntD1"; val IntD2 = thm "IntD2"; val IntE = thm "IntE"; val IntI = thm "IntI"; val Int_Collect = thm "Int_Collect"; val Int_Collect_mono = thm "Int_Collect_mono"; val Int_Diff = thm "Int_Diff"; val Int_Inter_image = thm "Int_Inter_image"; val Int_UNIV = thm "Int_UNIV"; val Int_UNIV_left = thm "Int_UNIV_left"; val Int_UNIV_right = thm "Int_UNIV_right"; val Int_UN_distrib = thm "Int_UN_distrib"; val Int_UN_distrib2 = thm "Int_UN_distrib2"; val Int_Un_distrib = thm "Int_Un_distrib"; val Int_Un_distrib2 = thm "Int_Un_distrib2"; val Int_Union = thm "Int_Union"; val Int_Union2 = thm "Int_Union2"; val Int_absorb = thm "Int_absorb"; val Int_absorb1 = thm "Int_absorb1"; val Int_absorb2 = thm "Int_absorb2"; val Int_ac = thms "Int_ac"; val Int_assoc = thm "Int_assoc"; val Int_commute = thm "Int_commute"; val Int_def = thm "Int_def"; val Int_empty_left = thm "Int_empty_left"; val Int_empty_right = thm "Int_empty_right"; val Int_eq_Inter = thm "Int_eq_Inter"; val Int_greatest = thm "Int_greatest"; val Int_iff = thm "Int_iff"; val Int_insert_left = thm "Int_insert_left"; val Int_insert_right = thm "Int_insert_right"; val Int_left_absorb = thm "Int_left_absorb"; val Int_left_commute = thm "Int_left_commute"; val Int_lower1 = thm "Int_lower1"; val Int_lower2 = thm "Int_lower2"; val Int_mono = thm "Int_mono"; val Int_subset_iff = thm "Int_subset_iff"; val InterD = thm "InterD"; val InterE = thm "InterE"; val InterI = thm "InterI"; val Inter_UNIV = thm "Inter_UNIV"; val Inter_Un_distrib = thm "Inter_Un_distrib"; val Inter_Un_subset = thm "Inter_Un_subset"; val Inter_anti_mono = thm "Inter_anti_mono"; val Inter_def = thm "Inter_def"; val Inter_empty = thm "Inter_empty"; val Inter_greatest = thm "Inter_greatest"; val Inter_iff = thm "Inter_iff"; val Inter_image_eq = thm "Inter_image_eq"; val Inter_insert = thm "Inter_insert"; val Inter_lower = thm "Inter_lower"; val PowD = thm "PowD"; val PowI = thm "PowI"; val Pow_Compl = thm "Pow_Compl"; val Pow_INT_eq = thm "Pow_INT_eq"; val Pow_Int_eq = thm "Pow_Int_eq"; val Pow_UNIV = thm "Pow_UNIV"; val Pow_bottom = thm "Pow_bottom"; val Pow_def = thm "Pow_def"; val Pow_empty = thm "Pow_empty"; val Pow_iff = thm "Pow_iff"; val Pow_insert = thm "Pow_insert"; val Pow_mono = thm "Pow_mono"; val Pow_top = thm "Pow_top"; val UNION_def = thm "UNION_def"; val UNIV_I = thm "UNIV_I"; val UNIV_def = thm "UNIV_def"; val UNIV_not_empty = thm "UNIV_not_empty"; val UNIV_witness = thm "UNIV_witness"; val UN_E = thm "UN_E"; val UN_I = thm "UN_I"; val UN_Pow_subset = thm "UN_Pow_subset"; val UN_UN_flatten = thm "UN_UN_flatten"; val UN_Un = thm "UN_Un"; val UN_Un_distrib = thm "UN_Un_distrib"; val UN_absorb = thm "UN_absorb"; val UN_bool_eq = thm "UN_bool_eq"; val UN_cong = thm "UN_cong"; val UN_constant = thm "UN_constant"; val UN_empty = thm "UN_empty"; val UN_empty2 = thm "UN_empty2"; val UN_eq = thm "UN_eq"; val UN_iff = thm "UN_iff"; val UN_insert = thm "UN_insert"; val UN_insert_distrib = thm "UN_insert_distrib"; val UN_least = thm "UN_least"; val UN_mono = thm "UN_mono"; val UN_simps = thms "UN_simps"; val UN_singleton = thm "UN_singleton"; val UN_subset_iff = thm "UN_subset_iff"; val UN_upper = thm "UN_upper"; val UnCI = thm "UnCI"; val UnE = thm "UnE"; val UnI1 = thm "UnI1"; val UnI2 = thm "UnI2"; val Un_Diff = thm "Un_Diff"; val Un_Diff_Int = thm "Un_Diff_Int"; val Un_Diff_cancel = thm "Un_Diff_cancel"; val Un_Diff_cancel2 = thm "Un_Diff_cancel2"; val Un_INT_distrib = thm "Un_INT_distrib"; val Un_INT_distrib2 = thm "Un_INT_distrib2"; val Un_Int_assoc_eq = thm "Un_Int_assoc_eq"; val Un_Int_crazy = thm "Un_Int_crazy"; val Un_Int_distrib = thm "Un_Int_distrib"; val Un_Int_distrib2 = thm "Un_Int_distrib2"; val Un_Inter = thm "Un_Inter"; val Un_Pow_subset = thm "Un_Pow_subset"; val Un_UNIV_left = thm "Un_UNIV_left"; val Un_UNIV_right = thm "Un_UNIV_right"; val Un_Union_image = thm "Un_Union_image"; val Un_absorb = thm "Un_absorb"; val Un_absorb1 = thm "Un_absorb1"; val Un_absorb2 = thm "Un_absorb2"; val Un_ac = thms "Un_ac"; val Un_assoc = thm "Un_assoc"; val Un_commute = thm "Un_commute"; val Un_def = thm "Un_def"; val Un_empty = thm "Un_empty"; val Un_empty_left = thm "Un_empty_left"; val Un_empty_right = thm "Un_empty_right"; val Un_eq_UN = thm "Un_eq_UN"; val Un_eq_Union = thm "Un_eq_Union"; val Un_iff = thm "Un_iff"; val Un_insert_left = thm "Un_insert_left"; val Un_insert_right = thm "Un_insert_right"; val Un_least = thm "Un_least"; val Un_left_absorb = thm "Un_left_absorb"; val Un_left_commute = thm "Un_left_commute"; val Un_mono = thm "Un_mono"; val Un_subset_iff = thm "Un_subset_iff"; val Un_upper1 = thm "Un_upper1"; val Un_upper2 = thm "Un_upper2"; val UnionE = thm "UnionE"; val UnionI = thm "UnionI"; val Union_Int_subset = thm "Union_Int_subset"; val Union_Pow_eq = thm "Union_Pow_eq"; val Union_UNIV = thm "Union_UNIV"; val Union_Un_distrib = thm "Union_Un_distrib"; val Union_def = thm "Union_def"; val Union_disjoint = thm "Union_disjoint"; val Union_empty = thm "Union_empty"; val Union_empty_conv = thm "Union_empty_conv"; val Union_iff = thm "Union_iff"; val Union_image_eq = thm "Union_image_eq"; val Union_insert = thm "Union_insert"; val Union_least = thm "Union_least"; val Union_mono = thm "Union_mono"; val Union_upper = thm "Union_upper"; val all_bool_eq = thm "all_bool_eq"; val all_mono = thm "all_mono"; val all_not_in_conv = thm "all_not_in_conv"; val atomize_ball = thm "atomize_ball"; val ballE = thm "ballE"; val ballI = thm "ballI"; val ball_UN = thm "ball_UN"; val ball_UNIV = thm "ball_UNIV"; val ball_Un = thm "ball_Un"; val ball_cong = thm "ball_cong"; val ball_conj_distrib = thm "ball_conj_distrib"; val ball_empty = thm "ball_empty"; val ball_one_point1 = thm "ball_one_point1"; val ball_one_point2 = thm "ball_one_point2"; val ball_simps = thms "ball_simps"; val ball_triv = thm "ball_triv"; val basic_monos = thms "basic_monos"; val bexCI = thm "bexCI"; val bexE = thm "bexE"; val bexI = thm "bexI"; val bex_UN = thm "bex_UN"; val bex_UNIV = thm "bex_UNIV"; val bex_Un = thm "bex_Un"; val bex_cong = thm "bex_cong"; val bex_disj_distrib = thm "bex_disj_distrib"; val bex_empty = thm "bex_empty"; val bex_one_point1 = thm "bex_one_point1"; val bex_one_point2 = thm "bex_one_point2"; val bex_simps = thms "bex_simps"; val bex_triv = thm "bex_triv"; val bex_triv_one_point1 = thm "bex_triv_one_point1"; val bex_triv_one_point2 = thm "bex_triv_one_point2"; val bool_induct = thm "bool_induct"; val bspec = thm "bspec"; val conj_mono = thm "conj_mono"; val contra_subsetD = thm "contra_subsetD"; val diff_single_insert = thm "diff_single_insert"; val disj_mono = thm "disj_mono"; val disjoint_eq_subset_Compl = thm "disjoint_eq_subset_Compl"; val disjoint_iff_not_equal = thm "disjoint_iff_not_equal"; val distinct_lemma = thm "distinct_lemma"; val double_complement = thm "double_complement"; val double_diff = thm "double_diff"; val emptyE = thm "emptyE"; val empty_Diff = thm "empty_Diff"; val empty_def = thm "empty_def"; val empty_iff = thm "empty_iff"; val empty_subsetI = thm "empty_subsetI"; val eq_to_mono = thm "eq_to_mono"; val eq_to_mono2 = thm "eq_to_mono2"; val eqset_imp_iff = thm "eqset_imp_iff"; val equalityCE = thm "equalityCE"; val equalityD1 = thm "equalityD1"; val equalityD2 = thm "equalityD2"; val equalityE = thm "equalityE"; val equalityI = thm "equalityI"; val equals0D = thm "equals0D"; val equals0I = thm "equals0I"; val ex_bool_eq = thm "ex_bool_eq"; val ex_mono = thm "ex_mono"; val full_SetCompr_eq = thm "full_SetCompr_eq"; val if_image_distrib = thm "if_image_distrib"; val imageE = thm "imageE"; val imageI = thm "imageI"; val image_Collect = thm "image_Collect"; val image_Un = thm "image_Un"; val image_Union = thm "image_Union"; val image_cong = thm "image_cong"; val image_constant = thm "image_constant"; val image_def = thm "image_def"; val image_empty = thm "image_empty"; val image_eqI = thm "image_eqI"; val image_iff = thm "image_iff"; val image_image = thm "image_image"; val image_insert = thm "image_insert"; val image_is_empty = thm "image_is_empty"; val image_mono = thm "image_mono"; val image_subsetI = thm "image_subsetI"; val image_subset_iff = thm "image_subset_iff"; val imp_mono = thm "imp_mono"; val imp_refl = thm "imp_refl"; val in_mono = thm "in_mono"; val insertCI = thm "insertCI"; val insertE = thm "insertE"; val insertI1 = thm "insertI1"; val insertI2 = thm "insertI2"; val insert_Collect = thm "insert_Collect"; val insert_Diff = thm "insert_Diff"; val insert_Diff1 = thm "insert_Diff1"; val insert_Diff_if = thm "insert_Diff_if"; val insert_absorb = thm "insert_absorb"; val insert_absorb2 = thm "insert_absorb2"; val insert_commute = thm "insert_commute"; val insert_def = thm "insert_def"; val insert_iff = thm "insert_iff"; val insert_image = thm "insert_image"; val insert_is_Un = thm "insert_is_Un"; val insert_mono = thm "insert_mono"; val insert_not_empty = thm "insert_not_empty"; val insert_subset = thm "insert_subset"; val mem_Collect_eq = thm "mem_Collect_eq"; val mem_simps = thms "mem_simps"; val mk_disjoint_insert = thm "mk_disjoint_insert"; val mono_Int = thm "mono_Int"; val mono_Un = thm "mono_Un"; val not_psubset_empty = thm "not_psubset_empty"; val psubsetI = thm "psubsetI"; val psubset_def = thm "psubset_def"; val psubset_eq = thm "psubset_eq"; val psubset_imp_ex_mem = thm "psubset_imp_ex_mem"; val psubset_imp_subset = thm "psubset_imp_subset"; val psubset_insert_iff = thm "psubset_insert_iff"; val psubset_subset_trans = thm "psubset_subset_trans"; val rangeE = thm "rangeE"; val rangeI = thm "rangeI"; val range_composition = thm "range_composition"; val range_eqI = thm "range_eqI"; val rev_bexI = thm "rev_bexI"; val rev_image_eqI = thm "rev_image_eqI"; val rev_subsetD = thm "rev_subsetD"; val set_diff_def = thm "set_diff_def"; val set_eq_subset = thm "set_eq_subset"; val set_ext = thm "set_ext"; val setup_induction = thm "setup_induction"; val singletonD = thm "singletonD"; val singletonE = thm "singletonE"; val singletonI = thm "singletonI"; val singleton_conv = thm "singleton_conv"; val singleton_conv2 = thm "singleton_conv2"; val singleton_iff = thm "singleton_iff"; val singleton_inject = thm "singleton_inject"; val singleton_insert_inj_eq = thm "singleton_insert_inj_eq"; val singleton_insert_inj_eq' = thm "singleton_insert_inj_eq'"; val split_if_eq1 = thm "split_if_eq1"; val split_if_eq2 = thm "split_if_eq2"; val split_if_mem1 = thm "split_if_mem1"; val split_if_mem2 = thm "split_if_mem2"; val split_ifs = thms "split_ifs"; val strip = thms "strip"; val subsetCE = thm "subsetCE"; val subsetD = thm "subsetD"; val subsetI = thm "subsetI"; val subset_Compl_self_eq = thm "subset_Compl_self_eq"; val subset_Pow_Union = thm "subset_Pow_Union"; val subset_UNIV = thm "subset_UNIV"; val subset_Un_eq = thm "subset_Un_eq"; val subset_antisym = thm "subset_antisym"; val subset_def = thm "subset_def"; val subset_empty = thm "subset_empty"; val subset_iff = thm "subset_iff"; val subset_iff_psubset_eq = thm "subset_iff_psubset_eq"; val subset_image_iff = thm "subset_image_iff"; val subset_insert = thm "subset_insert"; val subset_insertI = thm "subset_insertI"; val subset_insert_iff = thm "subset_insert_iff"; val subset_psubset_trans = thm "subset_psubset_trans"; val subset_refl = thm "subset_refl"; val subset_singletonD = thm "subset_singletonD"; val subset_trans = thm "subset_trans"; val vimageD = thm "vimageD"; val vimageE = thm "vimageE"; val vimageI = thm "vimageI"; val vimageI2 = thm "vimageI2"; val vimage_Collect = thm "vimage_Collect"; val vimage_Collect_eq = thm "vimage_Collect_eq"; val vimage_Compl = thm "vimage_Compl"; val vimage_Diff = thm "vimage_Diff"; val vimage_INT = thm "vimage_INT"; val vimage_Int = thm "vimage_Int"; val vimage_UN = thm "vimage_UN"; val vimage_UNIV = thm "vimage_UNIV"; val vimage_Un = thm "vimage_Un"; val vimage_Union = thm "vimage_Union"; val vimage_def = thm "vimage_def"; val vimage_empty = thm "vimage_empty"; val vimage_eq = thm "vimage_eq"; val vimage_eq_UN = thm "vimage_eq_UN"; val vimage_insert = thm "vimage_insert"; val vimage_mono = thm "vimage_mono"; val vimage_singleton_eq = thm "vimage_singleton_eq"; structure Set = struct val thy = the_context (); val Ball_def = Ball_def; val Bex_def = Bex_def; val Collect_mem_eq = Collect_mem_eq; val Compl_def = Compl_def; val INTER_def = INTER_def; val Int_def = Int_def; val Inter_def = Inter_def; val Pow_def = Pow_def; val UNION_def = UNION_def; val UNIV_def = UNIV_def; val Un_def = Un_def; val Union_def = Union_def; val empty_def = empty_def; val image_def = image_def; val insert_def = insert_def; val mem_Collect_eq = mem_Collect_eq; val psubset_def = psubset_def; val set_diff_def = set_diff_def; val subset_def = subset_def; end;