# HG changeset patch
# User wenzelm
# Date 1183917115 -7200
# Node ID a2ad1c166ac8b736cb1f18259e55bcb519196a01
# Parent  560f8f41ade2d83ad36dc6f671c7ed5d95009ec0
attribute tagged: single argument;

diff -r 560f8f41ade2 -r a2ad1c166ac8 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sun Jul 08 19:51:54 2007 +0200
+++ b/doc-src/IsarRef/generic.tex	Sun Jul 08 19:51:55 2007 +0200
@@ -832,7 +832,7 @@
 \end{matharray}
 
 \begin{rail}
-  'tagged' (nameref+)
+  'tagged' nameref
   ;
   'untagged' name
   ;
@@ -844,11 +844,11 @@
 
 \begin{descr}
 
-\item [$tagged~name~args$ and $untagged~name$] add and remove $tags$ of some
+\item [$tagged~name~arg$ and $untagged~name$] add and remove $tags$ of some
   theorem.  Tags may be any list of strings that serve as comment for some
   tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
-  result).  The first string is considered the tag name, the rest its
-  arguments.  Note that untag removes any tags of the same name.
+  result).  The first string is considered the tag name, the second its
+  argument.  Note that $untagged$ removes any tags of the same name.
 
 \item [$THEN~a$ and $COMP~a$] compose rules by resolution.  $THEN$ resolves
   with the first premise of $a$ (an alternative position may be also