# HG changeset patch
# User haftmann
# Date 1252070391 -7200
# Node ID 4942abb40a55d5c6d5fd9b2839d00bcdb90a036a
# Parent  e3c4e337196c5bbd1d529a3a69c72689e0d1d616# Parent  e9644b497e1cb3f2e62aa1e4eef6e479c46129ed
merged

diff -r e3c4e337196c -r 4942abb40a55 src/HOL/MetisExamples/set.thy
--- a/src/HOL/MetisExamples/set.thy	Fri Sep 04 13:57:56 2009 +0200
+++ b/src/HOL/MetisExamples/set.thy	Fri Sep 04 15:19:51 2009 +0200
@@ -238,7 +238,7 @@
 
 lemma (*singleton_example_2:*)
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_eq)
+by (metis Set.subsetI Union_upper insert_code mem_def set_eq_subset)
 
 lemma singleton_example_2:
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
@@ -275,8 +275,8 @@
 apply (metis emptyE)
 apply (metis insert_iff singletonE)
 apply (metis insertCI singletonE zless_le)
-apply (metis insert_iff singletonE)
-apply (metis insert_iff singletonE)
+apply (metis Collect_def Collect_mem_eq)
+apply (metis Collect_def Collect_mem_eq)
 apply (metis DiffE)
 apply (metis pair_in_Id_conv) 
 done