author nipkow Sun, 11 Nov 2018 14:34:02 +0100 changeset 69285 b9dd40e2c470 parent 69283 39044da8bb5a (current diff) parent 69284 3273692de24a (diff) child 69286 e4d5a07fecb6
merged
```--- a/src/HOL/Analysis/Sigma_Algebra.thy	Sun Nov 11 12:13:24 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Sun Nov 11 14:34:02 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"```
```--- a/src/HOL/Set.thy	Sun Nov 11 12:13:24 2018 +0100
+++ b/src/HOL/Set.thy	Sun Nov 11 14:34:02 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"```