--- a/src/Doc/IsarRef/Inner_Syntax.thy Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/IsarRef/Inner_Syntax.thy Fri Jan 17 20:20:20 2014 +0100
@@ -561,9 +561,9 @@
@{rail "
(@@{command type_notation} | @@{command no_type_notation}) @{syntax target}?
- @{syntax mode}? \\ (@{syntax nameref} @{syntax mixfix} + @'and')
+ @{syntax mode}? \<newline> (@{syntax nameref} @{syntax mixfix} + @'and')
;
- (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \\
+ (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \<newline>
(@{syntax nameref} @{syntax mixfix} + @'and')
;
@@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')