diff -r 6ab174bfefe2 -r 3f19e324ff59 doc-src/IsarRef/Thy/Generic.thy --- a/doc-src/IsarRef/Thy/Generic.thy Thu May 05 15:01:32 2011 +0200 +++ b/doc-src/IsarRef/Thy/Generic.thy Thu May 05 23:15:11 2011 +0200 @@ -189,7 +189,7 @@ \end{matharray} @{rail " - @@{method subst} ('(' 'asm' ')')? ('(' (@{syntax nat}+) ')')? @{syntax thmref} + @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref} ; @@{method split} ('(' 'asm' ')')? @{syntax thmrefs} "} @@ -292,7 +292,7 @@ @{rail " (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} | - @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goalspec}? + @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goalspec}? \\ ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} ) ; @@{method subgoal_tac} @{syntax goalspec}? (@{syntax prop} +)