--- a/doc-src/IsarRef/Thy/Generic.thy Tue Aug 09 09:39:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Tue Aug 09 15:41:00 2011 +0200
@@ -201,7 +201,7 @@
@{rail "
@@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref}
;
- @@{method split} ('(' 'asm' ')')? @{syntax thmrefs}
+ @@{method split} @{syntax thmrefs}
"}
These methods provide low-level facilities for equational reasoning
@@ -245,12 +245,13 @@
t"} where @{text x} is a free or bound variable.
\item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case
- splitting using the given rules. By default, splitting is performed
- in the conclusion of a goal; the @{text "(asm)"} option indicates to
- operate on assumptions instead.
+ splitting using the given rules. Splitting is performed in the
+ conclusion or some assumption of the subgoal, depending of the
+ structure of the rule.
Note that the @{method simp} method already involves repeated
- application of split rules as declared in the current context.
+ application of split rules as declared in the current context, using
+ @{attribute split}, for example.
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/Generic.tex Tue Aug 09 09:39:49 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Tue Aug 09 15:41:00 2011 +0200
@@ -336,14 +336,8 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
\rail@end
-\rail@begin{2}{}
+\rail@begin{1}{}
\rail@term{\hyperlink{method.split}{\mbox{\isa{split}}}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@term{\isa{asm}}[]
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@endbar
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
\end{railoutput}
@@ -388,12 +382,13 @@
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.
\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
- splitting using the given rules. By default, splitting is performed
- in the conclusion of a goal; the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option indicates to
- operate on assumptions instead.
+ splitting using the given rules. Splitting is performed in the
+ conclusion or some assumption of the subgoal, depending of the
+ structure of the rule.
Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated
- application of split rules as declared in the current context.
+ application of split rules as declared in the current context, using
+ \hyperlink{attribute.split}{\mbox{\isa{split}}}, for example.
\end{description}%
\end{isamarkuptext}%