diff -r 94fa3376ba33 -r 3273692de24a src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Nov 10 19:39:38 2018 +0100
+++ b/src/HOL/Set.thy	Sun Nov 11 13:05:15 2018 +0100
@@ -1122,7 +1122,7 @@
 
 text \<open>\<^medskip> Set difference.\<close>
 
-lemma Diff_subset: "A - B \<subseteq> A"
+lemma Diff_subset[simp]: "A - B \<subseteq> A"
   by blast
 
 lemma Diff_subset_conv: "A - B \<subseteq> C \<longleftrightarrow> A \<subseteq> B \<union> C"