diff -r 00e849f5b397 -r 61a6bf7d4b02 src/Doc/IsarRef/Inner_Syntax.thy
--- 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')