--- a/src/ZF/upair.thy Sun Oct 07 15:49:25 2007 +0200
+++ b/src/ZF/upair.thy Sun Oct 07 21:19:31 2007 +0200
@@ -525,95 +525,4 @@
"Inter({b}) = b"
by blast+
-
-ML
-{*
-val Upair_iff = thm "Upair_iff";
-val UpairI1 = thm "UpairI1";
-val UpairI2 = thm "UpairI2";
-val UpairE = thm "UpairE";
-val Un_iff = thm "Un_iff";
-val UnI1 = thm "UnI1";
-val UnI2 = thm "UnI2";
-val UnE = thm "UnE";
-val UnE' = thm "UnE'";
-val UnCI = thm "UnCI";
-val Int_iff = thm "Int_iff";
-val IntI = thm "IntI";
-val IntD1 = thm "IntD1";
-val IntD2 = thm "IntD2";
-val IntE = thm "IntE";
-val Diff_iff = thm "Diff_iff";
-val DiffI = thm "DiffI";
-val DiffD1 = thm "DiffD1";
-val DiffD2 = thm "DiffD2";
-val DiffE = thm "DiffE";
-val cons_iff = thm "cons_iff";
-val consI1 = thm "consI1";
-val consI2 = thm "consI2";
-val consE = thm "consE";
-val consE' = thm "consE'";
-val consCI = thm "consCI";
-val cons_not_0 = thm "cons_not_0";
-val cons_neq_0 = thm "cons_neq_0";
-val singleton_iff = thm "singleton_iff";
-val singletonI = thm "singletonI";
-val singletonE = thm "singletonE";
-val the_equality = thm "the_equality";
-val the_equality2 = thm "the_equality2";
-val theI = thm "theI";
-val the_0 = thm "the_0";
-val theI2 = thm "theI2";
-val if_true = thm "if_true";
-val if_false = thm "if_false";
-val if_cong = thm "if_cong";
-val if_weak_cong = thm "if_weak_cong";
-val if_P = thm "if_P";
-val if_not_P = thm "if_not_P";
-val split_if = thm "split_if";
-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 if_iff = thm "if_iff";
-val if_type = thm "if_type";
-val mem_asym = thm "mem_asym";
-val mem_irrefl = thm "mem_irrefl";
-val mem_not_refl = thm "mem_not_refl";
-val mem_imp_not_eq = thm "mem_imp_not_eq";
-val succ_iff = thm "succ_iff";
-val succI1 = thm "succI1";
-val succI2 = thm "succI2";
-val succE = thm "succE";
-val succCI = thm "succCI";
-val succ_not_0 = thm "succ_not_0";
-val succ_neq_0 = thm "succ_neq_0";
-val succ_subsetD = thm "succ_subsetD";
-val succ_neq_self = thm "succ_neq_self";
-val succ_inject_iff = thm "succ_inject_iff";
-val succ_inject = thm "succ_inject";
-
-val split_ifs = thms "split_ifs";
-val ball_simps = thms "ball_simps";
-val bex_simps = thms "bex_simps";
-
-val ball_conj_distrib = thm "ball_conj_distrib";
-val bex_disj_distrib = thm "bex_disj_distrib";
-val bex_triv_one_point1 = thm "bex_triv_one_point1";
-val bex_triv_one_point2 = thm "bex_triv_one_point2";
-val bex_one_point1 = thm "bex_one_point1";
-val bex_one_point2 = thm "bex_one_point2";
-val ball_one_point1 = thm "ball_one_point1";
-val ball_one_point2 = thm "ball_one_point2";
-
-val Rep_simps = thms "Rep_simps";
-val misc_simps = thms "misc_simps";
-
-val UN_simps = thms "UN_simps";
-val INT_simps = thms "INT_simps";
-
-val UN_extend_simps = thms "UN_extend_simps";
-val INT_extend_simps = thms "INT_extend_simps";
-*}
-
end