diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Analysis/Binary_Product_Measure.thy
--- a/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -16,7 +16,7 @@
 
 subsection "Binary products"
 
-definition\<^marker>\<open>tag important\<close> pair_measure (infixr "\<Otimes>\<^sub>M" 80) where
+definition\<^marker>\<open>tag important\<close> pair_measure (infixr \<open>\<Otimes>\<^sub>M\<close> 80) where
   "A \<Otimes>\<^sub>M B = measure_of (space A \<times> space B)
       {a \<times> b | a b. a \<in> sets A \<and> b \<in> sets B}
       (\<lambda>X. \<integral>\<^sup>+x. (\<integral>\<^sup>+y. indicator X (x,y) \<partial>B) \<partial>A)"