Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Probability/Measure_Space.thy
changeset 59048 7dc8ac6f0895
parent 59011 4902a2fec434
child 59425 c5e79df8cc21 
--- a/src/HOL/Probability/Measure_Space.thy	Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Mon Nov 24 12:20:14 2014 +0100
@@ -1180,7 +1180,7 @@
   "distr M N f = measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
 
 lemma
-  shows sets_distr[simp]: "sets (distr M N f) = sets N"
+  shows sets_distr[simp, measurable_cong]: "sets (distr M N f) = sets N"
     and space_distr[simp]: "space (distr M N f) = space N"
   by (auto simp: distr_def)
isabelle