| changeset 80786 | 70076ba563d2 |
| parent 76987 | 4c275405faae |
| child 80914 | d97fdabd9e2b |
--- a/src/Doc/Datatypes/Datatypes.thy Wed Aug 28 20:46:45 2024 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Aug 28 22:54:45 2024 +0200 @@ -453,7 +453,7 @@ Incidentally, this is how the traditional syntax can be set up: \<close> - syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]") + syntax "_list" :: "list_args \<Rightarrow> 'a list" ("[(_)]") text \<open>\blankline\<close>