--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Oct 29 12:30:15 2024 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Oct 29 21:51:21 2024 +0100
@@ -419,13 +419,13 @@
\<^item> @{notation_kind_def mixfix}: general mixfix notation, with delimiters
surrounding its arguments.
- \<^item> @{notation_kind_def prefix}: notation with delimiters before its
- arguments.
+ \<^item> @{notation_kind_def prefix}: notation with delimiter before its
+ argument.
- \<^item> @{notation_kind_def postfix}: notation with delimiters after its
- arguments.
+ \<^item> @{notation_kind_def postfix}: notation with delimiter after its
+ argument.
- \<^item> @{notation_kind_def "infix"}: notation with delimiters between its
+ \<^item> @{notation_kind_def "infix"}: notation with delimiter between its
arguments (automatically inserted for @{keyword "infix"} annotations,
see \secref{sec:infixes}).