# HG changeset patch
# User bulwahn
# Date 1329404522 -3600
# Node ID cd4832aa22293466212ecb57754db6e82fdeec7f
# Parent  fe51817749d190b8685f9c5b0cf92f98869aefc3
removing unnecessary premise from diff_single_insert

diff -r fe51817749d1 -r cd4832aa2229 src/HOL/Set.thy
--- 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)"