diff -r 965769fe2b63 -r fc1556774cfe src/HOL/Probability/Convolution.thy
--- a/src/HOL/Probability/Convolution.thy	Mon Dec 07 16:48:10 2015 +0000
+++ b/src/HOL/Probability/Convolution.thy	Mon Dec 07 20:19:59 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Sudeep Kanav, TU München
     Author:     Johannes Hölzl, TU München *)
 
-section {* Convolution Measure *}
+section \<open>Convolution Measure\<close>
 
 theory Convolution
   imports Independent_Family
@@ -160,7 +160,7 @@
       by (subst nn_integral_real_affine[where c=1 and t="-y"])
          (auto simp del: gt_0 simp add: one_ereal_def[symmetric])
     also have "\<dots> = (\<integral>\<^sup>+x. g y * (f (x - y) * indicator A x) \<partial>lborel)"
-      using `0 \<le> g y` by (intro nn_integral_cmult[symmetric]) auto
+      using \<open>0 \<le> g y\<close> by (intro nn_integral_cmult[symmetric]) auto
     finally show "(\<integral>\<^sup>+ x. g y * (f x * indicator A (x + y)) \<partial>lborel) =
       (\<integral>\<^sup>+ x. f (x - y) * g y * indicator A x \<partial>lborel)"
       by (simp add: ac_simps)