# 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 \ \ \ A \ D \ M" moreover have "(\ - A) \ D = (\ - (A \ D)) - (\ - D)" by auto - ultimately show "\ - A \ \ \ (\ - A) \ D \ M" + ultimately show "(\ - A) \ D \ M" using \D \ M\ by (auto intro: diff) next fix A :: "nat \ '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 \\<^medskip> Set difference.\ -lemma Diff_subset: "A - B \ A" +lemma Diff_subset[simp]: "A - B \ A" by blast lemma Diff_subset_conv: "A - B \ C \ A \ B \ C"