1.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Thu May 05 15:01:32 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Thu May 05 23:15:11 2011 +0200
     1.3 @@ -917,19 +917,19 @@
     1.4    \end{description}
     1.5  *}
     1.6  
     1.7 -    method_setup my_method1 = {*
     1.8 -      Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))
     1.9 -    *}  "my first method (without any arguments)"
    1.10 +  method_setup my_method1 = {*
    1.11 +    Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))
    1.12 +  *}  "my first method (without any arguments)"
    1.13  
    1.14 -    method_setup my_method2 = {*
    1.15 -      Scan.succeed (fn ctxt: Proof.context =>
    1.16 -        SIMPLE_METHOD' (fn i: int => no_tac))
    1.17 -    *}  "my second method (with context)"
    1.18 +  method_setup my_method2 = {*
    1.19 +    Scan.succeed (fn ctxt: Proof.context =>
    1.20 +      SIMPLE_METHOD' (fn i: int => no_tac))
    1.21 +  *}  "my second method (with context)"
    1.22  
    1.23 -    method_setup my_method3 = {*
    1.24 -      Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
    1.25 -        SIMPLE_METHOD' (fn i: int => no_tac))
    1.26 -    *}  "my third method (with theorem arguments and context)"
    1.27 +  method_setup my_method3 = {*
    1.28 +    Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
    1.29 +      SIMPLE_METHOD' (fn i: int => no_tac))
    1.30 +  *}  "my third method (with theorem arguments and context)"
    1.31  
    1.32  
    1.33  section {* Generalized elimination \label{sec:obtain} *}
    1.34 @@ -1275,7 +1275,8 @@
    1.35    ``strengthened'' inductive statements within the object-logic.
    1.36  
    1.37    @{rail "
    1.38 -    @@{method cases} ('(' 'no_simp' ')')? (@{syntax insts} * @'and') rule?
    1.39 +    @@{method cases} ('(' 'no_simp' ')')? \\
    1.40 +      (@{syntax insts} * @'and') rule?
    1.41      ;
    1.42      @@{method induct} ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
    1.43      ;