# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1450190507 0
# Node ID f8741f200f9141f4b81034495df7bcc229d3a653
# Parent  9250e546ab23f5c69895fa58833579ca2fb6cad8# Parent  9e38cde3d6726d790db9c2cbdb386f99e4accf9a
Merge

diff -r 9250e546ab23 -r f8741f200f91 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Dec 15 14:40:36 2015 +0000
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Dec 15 14:41:47 2015 +0000
@@ -1700,7 +1700,7 @@
 
 subsubsection \<open>Measurable functions\<close>
 
-definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" where
+definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>M" 60) where
   "measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
 
 lemma measurableI: