--- a/src/Doc/IsarRef/Proof.thy Fri Jan 17 18:12:35 2014 +0100
+++ b/src/Doc/IsarRef/Proof.thy Fri Jan 17 20:20:20 2014 +0100
@@ -190,7 +190,8 @@
;
@@{command def} (def + @'and')
;
- def: @{syntax thmdecl}? \\ @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
+ def: @{syntax thmdecl}? \<newline>
+ @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
"}
\begin{description}
@@ -1303,10 +1304,11 @@
command.
@{rail "
- @@{method cases} ('(' 'no_simp' ')')? \\
+ @@{method cases} ('(' 'no_simp' ')')? \<newline>
(@{syntax insts} * @'and') rule?
;
- (@@{method induct} | @@{method induction}) ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
+ (@@{method induct} | @@{method induction})
+ ('(' 'no_simp' ')')? (definsts * @'and') \<newline> arbitrary? taking? rule?
;
@@{method coinduct} @{syntax insts} taking rule?
;