equal
deleted
inserted
replaced
451 text \<open> |
451 text \<open> |
452 \noindent |
452 \noindent |
453 Incidentally, this is how the traditional syntax can be set up: |
453 Incidentally, this is how the traditional syntax can be set up: |
454 \<close> |
454 \<close> |
455 |
455 |
456 syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]") |
456 syntax "_list" :: "list_args \<Rightarrow> 'a list" ("[(_)]") |
457 |
457 |
458 text \<open>\blankline\<close> |
458 text \<open>\blankline\<close> |
459 |
459 |
460 translations |
460 translations |
461 "[x, xs]" == "x # [xs]" |
461 "[x, xs]" == "x # [xs]" |