# HG changeset patch
# User boehmes
# Date 1252164905 -7200
# Node ID 9f2784eae302b4bcc36600a56441dcd22010bacd
# Parent  ba397aa0ff5d5eefc56052111490e2a5279fc623# Parent  4942abb40a55d5c6d5fd9b2839d00bcdb90a036a
merged

diff -r ba397aa0ff5d -r 9f2784eae302 src/HOL/MetisExamples/set.thy
--- a/src/HOL/MetisExamples/set.thy	Sat Sep 05 17:34:30 2009 +0200
+++ b/src/HOL/MetisExamples/set.thy	Sat Sep 05 17:35:05 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