equal
deleted
inserted
replaced
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>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>[_\<^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 |
|
29 lazy_llist |
|
30 translations |
28 translations |
31 "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]" |
29 "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]" |
32 "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]" |
30 "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]" |
33 "\<^bold>[x\<^bold>]" == "CONST lazy_llist x" |
31 "\<^bold>[x\<^bold>]" == "CONST lazy_llist x" |
34 |
32 |