--- a/src/HOL/Analysis/Finite_Product_Measure.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Fri Sep 20 19:51:08 2024 +0200
@@ -169,7 +169,7 @@
"Pi\<^sub>M I M \<equiv> PiM I M"
syntax
- "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" ("(3\<Pi>\<^sub>M _\<in>_./ _)" 10)
+ "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" (\<open>(3\<Pi>\<^sub>M _\<in>_./ _)\<close> 10)
syntax_consts
"_PiM" == PiM
translations