# HG changeset patch
# User haftmann
# Date 1252070315 -7200
# Node ID e9644b497e1cb3f2e62aa1e4eef6e479c46129ed
# Parent  a579bc82e932a1ced905418a7a19ffd6f6fa0ec7
tuned metis proofs

diff -r a579bc82e932 -r e9644b497e1c src/HOL/MetisExamples/set.thy
--- a/src/HOL/MetisExamples/set.thy	Thu Sep 03 22:48:18 2009 +0200
+++ b/src/HOL/MetisExamples/set.thy	Fri Sep 04 15:18:35 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