# HG changeset patch
# User nipkow
# Date 1541937915 -3600
# Node ID 3273692de24a411be04cdd918e8f3b5017f84380
# Parent  94fa3376ba33a7768fefcb8183420c34390e33b6
more [simp]

diff -r 94fa3376ba33 -r 3273692de24a src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Sat Nov 10 19:39:38 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Sun Nov 11 13:05:15 2018 +0100
@@ -1333,7 +1333,7 @@
   fix A assume "A \<subseteq> \<Omega> \<and> A \<inter> D \<in> M"
   moreover have "(\<Omega> - A) \<inter> D = (\<Omega> - (A \<inter> D)) - (\<Omega> - D)"
     by auto
-  ultimately show "\<Omega> - A \<subseteq> \<Omega> \<and> (\<Omega> - A) \<inter> D \<in> M"
+  ultimately show "(\<Omega> - A) \<inter> D \<in> M"
     using  \<open>D \<in> M\<close> by (auto intro: diff)
 next
   fix A :: "nat \<Rightarrow> 'a set"
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"