equal
deleted
inserted
replaced
18 |
18 |
19 text \<open>List enumeration\<close> |
19 text \<open>List enumeration\<close> |
20 |
20 |
21 syntax |
21 syntax |
22 "_list" :: "args => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>) |
22 "_list" :: "args => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>) |
|
23 syntax_consts |
|
24 "_list" \<rightleftharpoons> Cons |
23 translations |
25 translations |
24 "[x, xs]" == "x#[xs]" |
26 "[x, xs]" == "x#[xs]" |
25 "[x]" == "x#[]" |
27 "[x]" == "x#[]" |
26 |
28 |
27 typedecl person |
29 typedecl person |