src/HOL/MetisExamples/set.thy
changeset 26806 40b411ec05aa
parent 26333 68e5eee47a45
child 28486 873726bdfd47
     1.1 --- a/src/HOL/MetisExamples/set.thy	Wed May 07 10:56:58 2008 +0200
     1.2 +++ b/src/HOL/MetisExamples/set.thy	Wed May 07 10:57:19 2008 +0200
     1.3 @@ -238,7 +238,7 @@
     1.4  
     1.5  lemma (*singleton_example_2:*)
     1.6       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
     1.7 -by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_def)
     1.8 +by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_eq)
     1.9  
    1.10  lemma singleton_example_2:
    1.11       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"