diff -r 0c898f7d9b15 -r 9e2eb05cc2b7 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Oct 05 15:18:49 2024 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Oct 05 22:24:24 2024 +0200
@@ -432,6 +432,9 @@
       its body argument (automatically inserted for @{keyword "binder"}
       annotations, see \secref{sec:binders}).
 
+      \<^item> @{notation_kind_def literal}: notation for literal values, such as
+      string or number.
+
       \<^item> @{notation_kind_def type_application}: application of a type
       constructor to its arguments.