src/HOL/HOLCF/Universal.thy

--- a/src/HOL/HOLCF/Universal.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/Universal.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -8,7 +8,7 @@
 imports Bifinite Completion "HOL-Library.Nat_Bijection"
 begin
 
-no_notation binomial  (infix "choose" 64)
+no_notation binomial  (infix \<open>choose\<close> 64)
 
 subsection \<open>Basis for universal domain\<close>
 
@@ -973,6 +973,6 @@
 
 hide_const (open) node
 
-notation binomial  (infixl "choose" 65)
+notation binomial  (infixl \<open>choose\<close> 65)
 
 end