1.1 --- a/doc-src/IsarRef/Thy/Generic.thy Thu May 15 17:37:20 2008 +0200
1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy Thu May 15 17:37:21 2008 +0200
1.3 @@ -1325,11 +1325,11 @@
1.4 facts, which are guaranteed to participate, may appear in either
1.5 order.
1.6
1.7 - \item [@{attribute intro} and @{attribute elim}] repeatedly refine
1.8 - some goal by intro- or elim-resolution, after having inserted any
1.9 - chained facts. Exactly the rules given as arguments are taken into
1.10 - account; this allows fine-tuned decomposition of a proof problem, in
1.11 - contrast to common automated tools.
1.12 + \item [@{method intro} and @{method elim}] repeatedly refine some
1.13 + goal by intro- or elim-resolution, after having inserted any chained
1.14 + facts. Exactly the rules given as arguments are taken into account;
1.15 + this allows fine-tuned decomposition of a proof problem, in contrast
1.16 + to common automated tools.
1.17
1.18 \end{descr}
1.19 *}