Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Code_Lazy_Demo.thy
changeset 80768 c7723cc15de8
parent 70009 435fb018e8ee
child 80786 70076ba563d2 
--- a/src/HOL/ex/Code_Lazy_Demo.thy	Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy	Sun Aug 25 21:10:01 2024 +0200
@@ -40,6 +40,7 @@
   | LCons (lhd: 'a) (ltl: "'a llist") (infixr "###" 65)
 
 syntax "_llist" :: "args => 'a list"    ("\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>")
+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>"
isabelle