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/Probability_Measure.thy
changeset 46905 6b1c0a80a57a
parent 46898 1570b30ee040
child 47694 05663f75964c 
--- a/src/HOL/Probability/Probability_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -260,7 +260,7 @@
 proof (rule prob_space_vimage)
   show "X \<in> measure_preserving M ?S"
     using X
-    unfolding measure_preserving_def distribution_def_raw
+    unfolding measure_preserving_def distribution_def [abs_def]
     by (auto simp: finite_measure_eq measurable_sets)
   show "sigma_algebra ?S" using X by simp
 qed
isabelle