
diff -r 07f64697408e -r 74d2e85f245d src/Doc/Isar_Ref/Inner_Syntax.thy
--- 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}).
 




