--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sun Sep 29 21:20:36 2024 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sun Sep 29 21:40:37 2024 +0200
@@ -1112,7 +1112,7 @@
;
mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
;
- syntaxdeps: (@{syntax name}+) ('==' | '\<rightleftharpoons>') (@{syntax name}+)
+ syntaxdeps: (((@{syntax name}+) ('==' | '\<rightleftharpoons>'))?) (@{syntax name}+)
;
transpat: ('(' @{syntax name} ')')? @{syntax string}
\<close>
@@ -1173,6 +1173,10 @@
specification of the effect of translation rules (see below) or translation
functions (see \secref{sec:tr-funs}).
+ @{command "syntax_types"}~\<open>types\<close> and @{command "syntax_consts"}~\<open>consts\<close>
+ merely declare formal entities to the inner-syntax engine, without any
+ dependencies yet.
+
\<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic translation rules
(i.e.\ macros) as first-order rewrite rules on ASTs (\secref{sec:ast}). The
theory context maintains two independent lists translation rules: parse