--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Fri Sep 20 19:51:08 2024 +0200
@@ -16,18 +16,18 @@
value [code] "cycle ''ab''"
value [code] "let x = cycle ''ab''; y = snth x 10 in x"
-datatype 'a llist = LNil ("\<^bold>[\<^bold>]") | LCons (lhd: 'a) (ltl: "'a llist") (infixr "\<^bold>#" 65)
+datatype 'a llist = LNil (\<open>\<^bold>[\<^bold>]\<close>) | LCons (lhd: 'a) (ltl: "'a llist") (infixr \<open>\<^bold>#\<close> 65)
subsection \<open>Finite lazy lists\<close>
code_lazy_type llist
-no_notation lazy_llist ("_")
+no_notation lazy_llist (\<open>_\<close>)
nonterminal llist_args
syntax
- "" :: "'a \<Rightarrow> llist_args" ("_")
- "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args" ("_,/ _")
- "_llist" :: "llist_args => 'a list" ("\<^bold>[(_)\<^bold>]")
+ "" :: "'a \<Rightarrow> llist_args" (\<open>_\<close>)
+ "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args" (\<open>_,/ _\<close>)
+ "_llist" :: "llist_args => 'a list" (\<open>\<^bold>[(_)\<^bold>]\<close>)
syntax_consts
"_llist_args" "_llist" == lazy_llist
translations
@@ -77,7 +77,7 @@
subsection \<open>Branching codatatypes\<close>
-codatatype tree = L | Node tree tree (infix "\<triangle>" 900)
+codatatype tree = L | Node tree tree (infix \<open>\<triangle>\<close> 900)
code_lazy_type tree