author wenzelm Sun Jul 08 19:51:55 2007 +0200 (2007-07-08) changeset 23654 a2ad1c166ac8 parent 23653 560f8f41ade2 child 23655 d2d1138e0ddc
attribute tagged: single argument;
     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