1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Tue Aug 09 09:39:49 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Tue Aug 09 15:41:00 2011 +0200
     1.3 @@ -201,7 +201,7 @@
     1.4    @{rail "
     1.5      @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref}
     1.6      ;
     1.7 -    @@{method split} ('(' 'asm' ')')? @{syntax thmrefs}
     1.8 +    @@{method split} @{syntax thmrefs}
     1.9    "}
    1.10  
    1.11    These methods provide low-level facilities for equational reasoning
    1.12 @@ -245,12 +245,13 @@
    1.13    t"} where @{text x} is a free or bound variable.
    1.14  
    1.15    \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case
    1.16 -  splitting using the given rules.  By default, splitting is performed
    1.17 -  in the conclusion of a goal; the @{text "(asm)"} option indicates to
    1.18 -  operate on assumptions instead.
    1.19 +  splitting using the given rules.  Splitting is performed in the
    1.20 +  conclusion or some assumption of the subgoal, depending of the
    1.21 +  structure of the rule.
    1.22    
    1.23    Note that the @{method simp} method already involves repeated
    1.24 -  application of split rules as declared in the current context.
    1.25 +  application of split rules as declared in the current context, using
    1.26 +  @{attribute split}, for example.
    1.27  
    1.28    \end{description}
    1.29  *}

     2.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Tue Aug 09 09:39:49 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Tue Aug 09 15:41:00 2011 +0200
     2.3 @@ -336,14 +336,8 @@
     2.4  \rail@endbar
     2.5  \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
     2.6  \rail@end
     2.7 -\rail@begin{2}{}
     2.8 +\rail@begin{1}{}
     2.9  \rail@term{\hyperlink{method.split}{\mbox{\isa{split}}}}[]
    2.10 -\rail@bar
    2.11 -\rail@nextbar{1}
    2.12 -\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
    2.13 -\rail@term{\isa{asm}}[]
    2.14 -\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
    2.15 -\rail@endbar
    2.16  \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
    2.17  \rail@end
    2.18  \end{railoutput}
    2.19 @@ -388,12 +382,13 @@
    2.20    assumption; this only works for equations of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} where \isa{x} is a free or bound variable.
    2.21  
    2.22    \item \hyperlink{method.split}{\mbox{\isa{split}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} performs single-step case
    2.23 -  splitting using the given rules.  By default, splitting is performed
    2.24 -  in the conclusion of a goal; the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option indicates to
    2.25 -  operate on assumptions instead.
    2.26 +  splitting using the given rules.  Splitting is performed in the
    2.27 +  conclusion or some assumption of the subgoal, depending of the
    2.28 +  structure of the rule.
    2.29    
    2.30    Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated
    2.31 -  application of split rules as declared in the current context.
    2.32 +  application of split rules as declared in the current context, using
    2.33 +  \hyperlink{attribute.split}{\mbox{\isa{split}}}, for example.
    2.34  
    2.35    \end{description}%
    2.36  \end{isamarkuptext}%