--- a/src/HOL/ex/Code_Lazy_Demo.thy Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy Fri Oct 18 14:20:09 2024 +0200
@@ -41,6 +41,8 @@
syntax
"_llist" :: "args => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>\<lbrakk>_\<^bold>\<rbrakk>)\<close>)
+syntax_consts
+ "_llist" == LCons
translations
"\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
"\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"