diff -r f6e595e4f608 -r 261cd8722677 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Sum_Type.thy	Mon Sep 23 13:32:38 2024 +0200
@@ -19,7 +19,7 @@
 
 definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
 
-typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool) set"
+typedef ('a, 'b) sum (infixr \<open>+\<close> 10) = "sum :: ('a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool) set"
   unfolding sum_def by auto
 
 lemma Inl_RepI: "Inl_Rep a \<in> sum"
@@ -209,7 +209,7 @@
 
 subsection \<open>The Disjoint Sum of Sets\<close>
 
-definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set"  (infixr "<+>" 65)
+definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set"  (infixr \<open><+>\<close> 65)
   where "A <+> B = Inl ` A \<union> Inr ` B"
 
 hide_const (open) Plus \<comment> \<open>Valuable identifier\<close>