Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorhaftmann
Fri, 04 Sep 2009 15:19:51 +0200
changeset 32520 4942abb40a55
parent 32518 e3c4e337196c (current diff)
parent 32519 e9644b497e1c (diff)
child 32524 9f2784eae302
merged
--- 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
isabelle