# HG changeset patch
# User Andreas Lochbihler
# Date 1421225952 -3600
# Node ID e6f5b1bbcb01e3060552d5d04c7aaf61944a0b87
# Parent  533f6cfc04c0de5d72f2e566aff2f1f697a4136b
allow line breaks in probability syntax

diff -r 533f6cfc04c0 -r e6f5b1bbcb01 src/HOL/Probability/Probability_Measure.thy
--- 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}"