--- a/src/HOL/Set.thy Wed Jan 06 16:17:50 2016 +0100
+++ b/src/HOL/Set.thy Thu Jan 07 17:40:55 2016 +0000
@@ -846,7 +846,10 @@
lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
by blast
-lemma diff_single_insert: "A - {x} \<subseteq> B ==> A \<subseteq> insert x B"
+lemma Diff_single_insert: "A - {x} \<subseteq> B ==> A \<subseteq> insert x B"
+ by blast
+
+lemma subset_Diff_insert: "A \<subseteq> B - (insert x C) \<longleftrightarrow> A \<subseteq> B - C \<and> x \<notin> A"
by blast
lemma doubleton_eq_iff: "({a,b} = {c,d}) = (a=c & b=d | a=d & b=c)"