# HG changeset patch
# User wenzelm
# Date 953329841 -3600
# Node ID d22fcea34cb7938e0d67cb2fab508f8af6f90208
# Parent  e2204e3df61bcea336eb3057caa46c8c7d54e1d3
untag: only name arg;
fixed trans att syntax;
tuned case command;

diff -r e2204e3df61b -r d22fcea34cb7 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Fri Mar 17 22:50:04 2000 +0100
+++ b/doc-src/IsarRef/generic.tex	Fri Mar 17 22:50:41 2000 +0100
@@ -82,7 +82,9 @@
 \end{matharray}
 
 \begin{rail}
-  ('tag' | 'untag') (nameref+)
+  'tag' (nameref+)
+  ;
+  'untag' name
   ;
   'OF' thmrefs
   ;
@@ -100,10 +102,11 @@
 \end{rail}
 
 \begin{descr}
-\item [$tag~tags$ and $untag~tags$] add and remove $tags$ of the theorem,
-  respectively.  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).
+\item [$tag~name~args$ and $untag~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.
 \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
   $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
   the reversed order).  Note that premises may be skipped by including
@@ -174,7 +177,7 @@
 \begin{rail}
   ('also' | 'finally') transrules? comment?
   ;
-  'trans' (() | 'add' ':' | 'del' ':') thmrefs
+  'trans' (() | 'add' | 'del')
   ;
 
   transrules: '(' thmrefs ')' interest?
@@ -230,8 +233,8 @@
 
 The $\CASENAME$ command provides a shorthand to refer to certain parts of
 logical context symbolically.  Proof methods may provide an environment of
-named ``cases'' of the form $c\colon \vec x, \vec \chi$.  Then the effect of
-$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\chi}$.
+named ``cases'' of the form $c\colon \vec x, \vec \phi$.  Then the effect of
+$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
 
 It is important to note that $\CASENAME$ does \emph{not} provide any means to
 peek at the current goal state, which is treated as strictly non-observable in
@@ -261,10 +264,10 @@
 \end{rail}
 
 \begin{descr}
-\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \chi$,
+\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$,
   as provided by an appropriate proof method (such as $cases$ and $induct$,
   see \S\ref{sec:induct-method}).  The command $\CASE{c}$ abbreviates
-  $\FIX{\vec x}~\ASSUME{c}{\vec\chi}$.
+  $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
 \item [$\isarkeyword{print_cases}$] prints all local contexts of the current
   goal context, using Isar proof language notation.  This is a diagnostic
   command; $undo$ does not apply.