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