author | wenzelm |
Thu, 16 Feb 2012 17:09:15 +0100 | |
changeset 46505 | cefceb54c656 |
parent 46504 | cd4832aa2229 (diff) |
parent 46503 | 186f4cab2ba0 (current diff) |
child 46506 | c7faa011bfa7 |
--- a/src/HOL/Set.thy Thu Feb 16 16:42:26 2012 +0100 +++ b/src/HOL/Set.thy Thu Feb 16 17:09:15 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)"