| changeset 69284 | 3273692de24a |
| parent 69216 | 1a52baa70aed |
| child 69546 | 27dae626822b |
--- 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"