diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/ex/Code_Lazy_Demo.thy
--- a/src/HOL/ex/Code_Lazy_Demo.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -13,7 +13,7 @@
 text \<open>Lazy evaluation for streams\<close>
 
 codatatype 'a stream = 
-  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
+  SCons (shd: 'a) (stl: "'a stream") (infixr \<open>##\<close> 65)
 
 primcorec up :: "nat \<Rightarrow> nat stream" where
   "up n = n ## up (n + 1)"
@@ -36,14 +36,14 @@
 text \<open>Lazy types need not be infinite. We can also have lazy types that are finite.\<close>
 
 datatype 'a llist
-  = LNil ("\<^bold>\<lbrakk>\<^bold>\<rbrakk>") 
-  | LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
+  = LNil (\<open>\<^bold>\<lbrakk>\<^bold>\<rbrakk>\<close>) 
+  | LCons (lhd: 'a) (ltl: "'a llist") (infixr \<open>###\<close> 65)
 
 nonterminal llist_args
 syntax
-  "" :: "'a \<Rightarrow> llist_args"  ("_")
-  "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  ("_,/ _")
-  "_llist" :: "llist_args => 'a list"    ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
+  "" :: "'a \<Rightarrow> llist_args"  (\<open>_\<close>)
+  "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  (\<open>_,/ _\<close>)
+  "_llist" :: "llist_args => 'a list"    (\<open>\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>\<close>)
 syntax_consts
   "_llist_args" "_llist" == LCons
 translations
@@ -81,7 +81,7 @@
   A conversion function to lazy lists is enough.\<close>
 
 primrec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist"
-  (infixr "@@" 65) where
+  (infixr \<open>@@\<close> 65) where
   "\<^bold>\<lbrakk>\<^bold>\<rbrakk> @@ ys = ys"
 | "(x ### xs) @@ ys = x ### (xs @@ ys)"
 
@@ -113,10 +113,10 @@
 section \<open>Branching datatypes\<close>
 
 datatype tree
-  = L              ("\<spadesuit>") 
-  | Node tree tree (infix "\<triangle>" 900)
+  = L              (\<open>\<spadesuit>\<close>) 
+  | Node tree tree (infix \<open>\<triangle>\<close> 900)
 
-notation (output) Node ("\<triangle>(//\<^bold>l: _//\<^bold>r: _)")
+notation (output) Node (\<open>\<triangle>(//\<^bold>l: _//\<^bold>r: _)\<close>)
 
 code_lazy_type tree