# HG changeset patch
# User wenzelm
# Date 1226609430 -3600
# Node ID b65194fe443485480e94734ea695d9d1d180de06
# Parent  b5e6122ff5756858a8ed860a0efc3777c85d1442
fixed/tuned syntax for attribute "tagged";

diff -r b5e6122ff575 -r b65194fe4434 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Thu Nov 13 21:49:46 2008 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy	Thu Nov 13 21:50:30 2008 +0100
@@ -120,7 +120,7 @@
   \end{matharray}
 
   \begin{rail}
-    'tagged' nameref
+    'tagged' name name
     ;
     'untagged' name
     ;
@@ -133,12 +133,11 @@
 
   \begin{description}
 
-  \item @{attribute tagged}~@{text "name arg"} and @{attribute
+  \item @{attribute tagged}~@{text "name value"} and @{attribute
   untagged}~@{text name} add and remove \emph{tags} of some theorem.
   Tags may be any list of string pairs that serve as formal comment.
-  The first string is considered the tag name, the second its
-  argument.  Note that @{attribute untagged} removes any tags of the
-  same name.
+  The first string is considered the tag name, the second its value.
+  Note that @{attribute untagged} removes any tags of the same name.
 
   \item @{attribute THEN}~@{text a} and @{attribute COMP}~@{text a}
   compose rules by resolution.  @{attribute THEN} resolves with the