--- a/src/HOL/Probability/Probability_Measure.thy Wed Jan 14 01:42:36 2015 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Wed Jan 14 09:59:12 2015 +0100
@@ -225,7 +225,7 @@
subsection {* Introduce binder for probability *}
syntax
- "_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'(_ in _. _'))")
+ "_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" ("('\<P>'((/_ in _./ _)'))")
translations
"\<P>(x in M. P)" => "CONST measure M {x \<in> CONST space M. P}"