# 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 \ logic \ logic \ logic" ("('\

'(_ in _. _'))") + "_prob" :: "pttrn \ logic \ logic \ logic" ("('\

'((/_ in _./ _)'))") translations "\

(x in M. P)" => "CONST measure M {x \ CONST space M. P}"