attribute tagged: single argument;
authorwenzelm
Sun Jul 08 19:51:55 2007 +0200 (2007-07-08)
changeset 23654a2ad1c166ac8
parent 23653 560f8f41ade2
child 23655 d2d1138e0ddc
attribute tagged: single argument;
doc-src/IsarRef/generic.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Sun Jul 08 19:51:54 2007 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sun Jul 08 19:51:55 2007 +0200
     1.3 @@ -832,7 +832,7 @@
     1.4  \end{matharray}
     1.5  
     1.6  \begin{rail}
     1.7 -  'tagged' (nameref+)
     1.8 +  'tagged' nameref
     1.9    ;
    1.10    'untagged' name
    1.11    ;
    1.12 @@ -844,11 +844,11 @@
    1.13  
    1.14  \begin{descr}
    1.15  
    1.16 -\item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some
    1.17 +\item [$tagged~name~arg$ and $untagged~name$] add and remove $tags$ of some
    1.18    theorem.  Tags may be any list of strings that serve as comment for some
    1.19    tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
    1.20 -  result).  The first string is considered the tag name, the rest its
    1.21 -  arguments.  Note that untag removes any tags of the same name.
    1.22 +  result).  The first string is considered the tag name, the second its
    1.23 +  argument.  Note that $untagged$ removes any tags of the same name.
    1.24  
    1.25  \item [$THEN~a$ and $COMP~a$] compose rules by resolution.  $THEN$ resolves
    1.26    with the first premise of $a$ (an alternative position may be also