| changeset 81090 | 843dba3d307a |
| parent 81019 | dd59daa3c37a |
| child 81093 | 9b11062b62c6 |
--- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 30 22:57:45 2024 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 30 23:32:26 2024 +0200 @@ -454,7 +454,7 @@ \<close> (*<*) no_syntax - "_list" :: "args => 'a list" (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>) + "_list" :: "args => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>) (*>*) syntax "_list" :: "args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)