--- a/src/HOL/Integ/Equiv.thy Tue Nov 18 09:45:45 2003 +0100
+++ b/src/HOL/Integ/Equiv.thy Tue Nov 18 11:01:52 2003 +0100
@@ -270,4 +270,46 @@
apply (simp_all add: Union_quotient equiv_type finite_quotient)
done
+ML
+{*
+
+(* legacy ML bindings *)
+
+val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
+val UN_constant_eq = thm "UN_constant_eq";
+val UN_equiv_class = thm "UN_equiv_class";
+val UN_equiv_class2 = thm "UN_equiv_class2";
+val UN_equiv_class_inject = thm "UN_equiv_class_inject";
+val UN_equiv_class_type = thm "UN_equiv_class_type";
+val UN_equiv_class_type2 = thm "UN_equiv_class_type2";
+val Union_quotient = thm "Union_quotient";
+val comp_equivI = thm "comp_equivI";
+val congruent2I = thm "congruent2I";
+val congruent2_commuteI = thm "congruent2_commuteI";
+val congruent2_def = thm "congruent2_def";
+val congruent2_implies_congruent = thm "congruent2_implies_congruent";
+val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";
+val congruent_def = thm "congruent_def";
+val eq_equiv_class = thm "eq_equiv_class";
+val eq_equiv_class_iff = thm "eq_equiv_class_iff";
+val equiv_class_eq = thm "equiv_class_eq";
+val equiv_class_eq_iff = thm "equiv_class_eq_iff";
+val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";
+val equiv_class_self = thm "equiv_class_self";
+val equiv_class_subset = thm "equiv_class_subset";
+val equiv_comp_eq = thm "equiv_comp_eq";
+val equiv_def = thm "equiv_def";
+val equiv_imp_dvd_card = thm "equiv_imp_dvd_card";
+val equiv_type = thm "equiv_type";
+val finite_equiv_class = thm "finite_equiv_class";
+val finite_quotient = thm "finite_quotient";
+val quotientE = thm "quotientE";
+val quotientI = thm "quotientI";
+val quotient_def = thm "quotient_def";
+val quotient_disj = thm "quotient_disj";
+val refl_comp_subset = thm "refl_comp_subset";
+val subset_equiv_class = thm "subset_equiv_class";
+val sym_trans_comp_subset = thm "sym_trans_comp_subset";
+*}
+
end