more [simp]
authornipkow
Sun Nov 11 13:05:15 2018 +0100 (11 months ago ago)
changeset 692893273692de24a
parent 69287 94fa3376ba33
child 69291 b9dd40e2c470
more [simp]
src/HOL/Analysis/Sigma_Algebra.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Sat Nov 10 19:39:38 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Sun Nov 11 13:05:15 2018 +0100
     1.3 @@ -1333,7 +1333,7 @@
     1.4    fix A assume "A \<subseteq> \<Omega> \<and> A \<inter> D \<in> M"
     1.5    moreover have "(\<Omega> - A) \<inter> D = (\<Omega> - (A \<inter> D)) - (\<Omega> - D)"
     1.6      by auto
     1.7 -  ultimately show "\<Omega> - A \<subseteq> \<Omega> \<and> (\<Omega> - A) \<inter> D \<in> M"
     1.8 +  ultimately show "(\<Omega> - A) \<inter> D \<in> M"
     1.9      using  \<open>D \<in> M\<close> by (auto intro: diff)
    1.10  next
    1.11    fix A :: "nat \<Rightarrow> 'a set"
     2.1 --- a/src/HOL/Set.thy	Sat Nov 10 19:39:38 2018 +0100
     2.2 +++ b/src/HOL/Set.thy	Sun Nov 11 13:05:15 2018 +0100
     2.3 @@ -1122,7 +1122,7 @@
     2.4  
     2.5  text \<open>\<^medskip> Set difference.\<close>
     2.6  
     2.7 -lemma Diff_subset: "A - B \<subseteq> A"
     2.8 +lemma Diff_subset[simp]: "A - B \<subseteq> A"
     2.9    by blast
    2.10  
    2.11  lemma Diff_subset_conv: "A - B \<subseteq> C \<longleftrightarrow> A \<subseteq> B \<union> C"