equal
deleted
inserted
replaced
38 datatype 'a llist |
38 datatype 'a llist |
39 = LNil (\<open>\<^bold>\<lbrakk>\<^bold>\<rbrakk>\<close>) |
39 = LNil (\<open>\<^bold>\<lbrakk>\<^bold>\<rbrakk>\<close>) |
40 | LCons (lhd: 'a) (ltl: "'a llist") (infixr \<open>###\<close> 65) |
40 | LCons (lhd: 'a) (ltl: "'a llist") (infixr \<open>###\<close> 65) |
41 |
41 |
42 syntax |
42 syntax |
43 "_llist" :: "args => 'a list" (\<open>\<^bold>\<lbrakk>(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>\<rbrakk>\<close>) |
43 "_llist" :: "args => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>\<lbrakk>_\<^bold>\<rbrakk>)\<close>) |
44 syntax_consts |
44 syntax_consts |
45 LCons |
45 LCons |
46 translations |
46 translations |
47 "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>" |
47 "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>" |
48 "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>" |
48 "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>" |