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/Information.thy
changeset 46905 6b1c0a80a57a
parent 46731 5302e932d1e5
child 47694 05663f75964c 
--- a/src/HOL/Probability/Information.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Probability/Information.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -823,7 +823,7 @@
   interpret S: prob_space "S\<lparr> measure := ereal\<circ>distribution X \<rparr>"
     using distribution_prob_space[OF X] .
   from A show "S.\<mu>' A = distribution X A"
-    unfolding S.\<mu>'_def by (simp add: distribution_def_raw \<mu>'_def)
+    unfolding S.\<mu>'_def by (simp add: distribution_def [abs_def] \<mu>'_def)
 qed
 
 lemma (in information_space) entropy_uniform_max:
isabelle