diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Library/ListVector.thy
--- a/src/HOL/Library/ListVector.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Library/ListVector.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -12,7 +12,7 @@
 
 text\<open>Multiplication with a scalar:\<close>
 
-abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)
+abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix \<open>*\<^sub>s\<close> 70)
 where "x *\<^sub>s xs \<equiv> map ((*) x) xs"
 
 lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
@@ -99,7 +99,7 @@
 
 subsection "Inner product"
 
-definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" ("\<langle>_,_\<rangle>") where
+definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" (\<open>\<langle>_,_\<rangle>\<close>) where
 "\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
 
 lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"