--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Mar 23 15:54:41 2015 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Mar 23 15:55:41 2015 +0100
@@ -521,10 +521,10 @@
entities within the current context.
@{rail \<open>
- (@@{command type_notation} | @@{command no_type_notation}) @{syntax target}?
- @{syntax mode}? \<newline> (@{syntax nameref} @{syntax mixfix} + @'and')
+ (@@{command type_notation} | @@{command no_type_notation}) @{syntax mode}? \<newline>
+ (@{syntax nameref} @{syntax mixfix} + @'and')
;
- (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \<newline>
+ (@@{command notation} | @@{command no_notation}) @{syntax mode}? \<newline>
(@{syntax nameref} @{syntax mixfix} + @'and')
;
@@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
@@ -1165,6 +1165,8 @@
@{attribute_def syntax_ast_stats} & : & @{text attribute} & default @{text false} \\
\end{tabular}
+ \medskip
+
Unlike mixfix notation for existing formal entities
(\secref{sec:notation}), raw syntax declarations provide full access
to the priority grammar of the inner syntax, without any sanity