equal
deleted
inserted
replaced
22 |
22 |
23 code_lazy_type llist |
23 code_lazy_type llist |
24 |
24 |
25 no_notation lazy_llist (\<open>_\<close>) |
25 no_notation lazy_llist (\<open>_\<close>) |
26 syntax |
26 syntax |
27 "_llist" :: "args => 'a list" (\<open>\<^bold>[(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>]\<close>) |
27 "_llist" :: "args => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>[_\<^bold>])\<close>) |
28 syntax_consts |
28 syntax_consts |
29 lazy_llist |
29 lazy_llist |
30 translations |
30 translations |
31 "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]" |
31 "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]" |
32 "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]" |
32 "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]" |