| changeset 46504 | cd4832aa2229 |
| parent 46459 | 73823dbbecc4 |
| child 46853 | 998ec26044c4 |
--- a/src/HOL/Set.thy Thu Feb 16 09:51:34 2012 +0100 +++ b/src/HOL/Set.thy Thu Feb 16 16:02:02 2012 +0100 @@ -871,7 +871,7 @@ lemma singleton_conv2 [simp]: "{x. a = x} = {a}" by blast -lemma diff_single_insert: "A - {x} \<subseteq> B ==> x \<in> A ==> A \<subseteq> insert x B" +lemma diff_single_insert: "A - {x} \<subseteq> B ==> A \<subseteq> insert x B" by blast lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"