diff -r f6e595e4f608 -r 261cd8722677 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Fun.thy	Mon Sep 23 13:32:38 2024 +0200
@@ -45,11 +45,11 @@
 
 subsection \<open>The Composition Operator \<open>f \<circ> g\<close>\<close>
 
-definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  (infixl "\<circ>" 55)
+definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  (infixl \<open>\<circ>\<close> 55)
   where "f \<circ> g = (\<lambda>x. f (g x))"
 
 notation (ASCII)
-  comp  (infixl "o" 55)
+  comp  (infixl \<open>o\<close> 55)
 
 lemma comp_apply [simp]: "(f \<circ> g) x = f (g x)"
   by (simp add: comp_def)
@@ -102,7 +102,7 @@
 
 subsection \<open>The Forward Composition Operator \<open>fcomp\<close>\<close>
 
-definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"  (infixl "\<circ>>" 60)
+definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c"  (infixl \<open>\<circ>>\<close> 60)
   where "f \<circ>> g = (\<lambda>x. g (f x))"
 
 lemma fcomp_apply [simp]:  "(f \<circ>> g) x = g (f x)"
@@ -123,7 +123,7 @@
 code_printing
   constant fcomp \<rightharpoonup> (Eval) infixl 1 "#>"
 
-no_notation fcomp (infixl "\<circ>>" 60)
+no_notation fcomp (infixl \<open>\<circ>>\<close> 60)
 
 
 subsection \<open>Mapping functions\<close>
@@ -841,10 +841,10 @@
 nonterminal updbinds and updbind
 
 syntax
-  "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind"             ("(2_ :=/ _)")
-  ""         :: "updbind \<Rightarrow> updbinds"             ("_")
-  "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" ("_,/ _")
-  "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"            ("_/'((_)')" [1000, 0] 900)
+  "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind"             (\<open>(2_ :=/ _)\<close>)
+  ""         :: "updbind \<Rightarrow> updbinds"             (\<open>_\<close>)
+  "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
+  "_Update"  :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"            (\<open>_/'((_)')\<close> [1000, 0] 900)
 
 syntax_consts
   "_updbind" "_updbinds" "_Update" \<rightleftharpoons> fun_upd