summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Probability/Giry_Monad.thy

changeset 59978 | c2dc7856e2e5 |

parent 59778 | fe5b796d6b2a |

child 60067 | f1a5bcf5658f |

--- a/src/HOL/Probability/Giry_Monad.thy Wed Apr 08 21:48:59 2015 +0200 +++ b/src/HOL/Probability/Giry_Monad.thy Wed Apr 08 21:49:45 2015 +0200 @@ -324,7 +324,7 @@ finally show ?thesis . qed -(* TODO: Rename. This name is too general – Manuel *) +(* TODO: Rename. This name is too general -- Manuel *) lemma measurable_pair_measure: assumes f: "f \<in> measurable M (subprob_algebra N)" assumes g: "g \<in> measurable M (subprob_algebra L)"