doc-src/IsarRef/Thy/Generic.thy
changeset 26901 d1694ef6e7a7
parent 26894 1120f6cc10b0
child 27040 3d3e6e07b931
     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  *}