diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Algebra/Indexed_Polynomials.thy
--- a/src/HOL/Algebra/Indexed_Polynomials.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Algebra/Indexed_Polynomials.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -23,13 +23,13 @@
 definition (in ring) indexed_const :: "'a \<Rightarrow> ('c multiset \<Rightarrow> 'a)" 
   where "indexed_const k = (\<lambda>m. if m = {#} then k else \<zero>)"
 
-definition (in ring) indexed_pmult :: "('c multiset \<Rightarrow> 'a) \<Rightarrow> 'c \<Rightarrow> ('c multiset \<Rightarrow> 'a)" (infixl "\<Otimes>" 65)
+definition (in ring) indexed_pmult :: "('c multiset \<Rightarrow> 'a) \<Rightarrow> 'c \<Rightarrow> ('c multiset \<Rightarrow> 'a)" (infixl \<open>\<Otimes>\<close> 65)
   where "indexed_pmult P i = (\<lambda>m. if i \<in># m then P (m - {# i #}) else \<zero>)"
 
-definition (in ring) indexed_padd :: "_ \<Rightarrow> _ \<Rightarrow> ('c multiset \<Rightarrow> 'a)" (infixl "\<Oplus>" 65)
+definition (in ring) indexed_padd :: "_ \<Rightarrow> _ \<Rightarrow> ('c multiset \<Rightarrow> 'a)" (infixl \<open>\<Oplus>\<close> 65)
   where "indexed_padd P Q = (\<lambda>m. (P m) \<oplus> (Q m))"
 
-definition (in ring) indexed_var :: "'c \<Rightarrow> ('c multiset \<Rightarrow> 'a)" ("\<X>\<index>")
+definition (in ring) indexed_var :: "'c \<Rightarrow> ('c multiset \<Rightarrow> 'a)" (\<open>\<X>\<index>\<close>)
   where "indexed_var i = (indexed_const \<one>) \<Otimes> i"
 
 definition (in ring) index_free :: "('c multiset \<Rightarrow> 'a) \<Rightarrow> 'c \<Rightarrow> bool"
@@ -38,7 +38,7 @@
 definition (in ring) carrier_coeff :: "('c multiset \<Rightarrow> 'a) \<Rightarrow> bool"
   where "carrier_coeff P \<longleftrightarrow> (\<forall>m. P m \<in> carrier R)"
 
-inductive_set (in ring) indexed_pset :: "'c set \<Rightarrow> 'a set \<Rightarrow> ('c multiset \<Rightarrow> 'a) set" ("_ [\<X>\<index>]" 80)
+inductive_set (in ring) indexed_pset :: "'c set \<Rightarrow> 'a set \<Rightarrow> ('c multiset \<Rightarrow> 'a) set" (\<open>_ [\<X>\<index>]\<close> 80)
   for I and K where
     indexed_const:  "k \<in> K \<Longrightarrow> indexed_const k \<in> (K[\<X>\<^bsub>I\<^esub>])"
   | indexed_padd:  "\<lbrakk> P \<in> (K[\<X>\<^bsub>I\<^esub>]); Q \<in> (K[\<X>\<^bsub>I\<^esub>]) \<rbrakk> \<Longrightarrow> P \<Oplus> Q \<in> (K[\<X>\<^bsub>I\<^esub>])"