merged
authorwenzelm
Thu, 16 Feb 2012 17:09:15 +0100
changeset 46505 cefceb54c656
parent 46504 cd4832aa2229 (diff)
parent 46503 186f4cab2ba0 (current diff)
child 46506 c7faa011bfa7
merged
--- 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)"