src/Doc/IsarRef/Generic.thy
changeset 55029 61a6bf7d4b02
parent 52060 179236c82c2a
child 55112 b1a5d603fd12
--- a/src/Doc/IsarRef/Generic.thy	Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/IsarRef/Generic.thy	Fri Jan 17 20:20:20 2014 +0100
@@ -202,7 +202,7 @@
   \end{matharray}
 
   @{rail "
-    @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref}
+    @@{method subst} ('(' 'asm' ')')? \<newline> ('(' (@{syntax nat}+) ')')? @{syntax thmref}
     ;
     @@{method split} @{syntax thmrefs}
   "}
@@ -306,7 +306,7 @@
 
   @{rail "
     (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
-      @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \\
+      @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \<newline>
     ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
     ;
     @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)
@@ -925,7 +925,7 @@
 
   @{rail "
     @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='
-      @{syntax text} \\ (@'identifier' (@{syntax nameref}+))?
+      @{syntax text} \<newline> (@'identifier' (@{syntax nameref}+))?
     ;
 
     @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)