removing unnecessary premise from diff_single_insert
authorbulwahn
Thu Feb 16 16:02:02 2012 +0100 (2012-02-16)
changeset 46504cd4832aa2229
parent 46501 fe51817749d1
child 46505 cefceb54c656
removing unnecessary premise from diff_single_insert
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Thu Feb 16 09:51:34 2012 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Feb 16 16:02:02 2012 +0100
     1.3 @@ -871,7 +871,7 @@
     1.4  lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
     1.5    by blast
     1.6  
     1.7 -lemma diff_single_insert: "A - {x} \<subseteq> B ==> x \<in> A ==> A \<subseteq> insert x B"
     1.8 +lemma diff_single_insert: "A - {x} \<subseteq> B ==> A \<subseteq> insert x B"
     1.9    by blast
    1.10  
    1.11  lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"