1.1 --- a/doc-src/IsarRef/generic.tex	Fri Mar 17 22:50:04 2000 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Fri Mar 17 22:50:41 2000 +0100
     1.3 @@ -82,7 +82,9 @@
     1.4  \end{matharray}
     1.5  
     1.6  \begin{rail}
     1.7 -  ('tag' | 'untag') (nameref+)
     1.8 +  'tag' (nameref+)
     1.9 +  ;
    1.10 +  'untag' name
    1.11    ;
    1.12    'OF' thmrefs
    1.13    ;
    1.14 @@ -100,10 +102,11 @@
    1.15  \end{rail}
    1.16  
    1.17  \begin{descr}
    1.18 -\item [$tag~tags$ and $untag~tags$] add and remove $tags$ of the theorem,
    1.19 -  respectively.  Tags may be any list of strings that serve as comment for
    1.20 -  some tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
    1.21 -  result).
    1.22 +\item [$tag~name~args$ and $untag~name$] add and remove $tags$ of some
    1.23 +  theorem.  Tags may be any list of strings that serve as comment for some
    1.24 +  tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
    1.25 +  result).  The first string is considered the tag name, the rest its
    1.26 +  arguments.  Note that untag removes any tags of the same name.
    1.27  \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
    1.28    $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
    1.29    the reversed order).  Note that premises may be skipped by including
    1.30 @@ -174,7 +177,7 @@
    1.31  \begin{rail}
    1.32    ('also' | 'finally') transrules? comment?
    1.33    ;
    1.34 -  'trans' (() | 'add' ':' | 'del' ':') thmrefs
    1.35 +  'trans' (() | 'add' | 'del')
    1.36    ;
    1.37  
    1.38    transrules: '(' thmrefs ')' interest?
    1.39 @@ -230,8 +233,8 @@
    1.40  
    1.41  The $\CASENAME$ command provides a shorthand to refer to certain parts of
    1.42  logical context symbolically.  Proof methods may provide an environment of
    1.43 -named ``cases'' of the form $c\colon \vec x, \vec \chi$.  Then the effect of
    1.44 -$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\chi}$.
    1.45 +named ``cases'' of the form $c\colon \vec x, \vec \phi$.  Then the effect of
    1.46 +$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
    1.47  
    1.48  It is important to note that $\CASENAME$ does \emph{not} provide any means to
    1.49  peek at the current goal state, which is treated as strictly non-observable in
    1.50 @@ -261,10 +264,10 @@
    1.51  \end{rail}
    1.52  
    1.53  \begin{descr}
    1.54 -\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \chi$,
    1.55 +\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$,
    1.56    as provided by an appropriate proof method (such as $cases$ and $induct$,
    1.57    see \S\ref{sec:induct-method}).  The command $\CASE{c}$ abbreviates
    1.58 -  $\FIX{\vec x}~\ASSUME{c}{\vec\chi}$.
    1.59 +  $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$.
    1.60  \item [$\isarkeyword{print_cases}$] prints all local contexts of the current
    1.61    goal context, using Isar proof language notation.  This is a diagnostic
    1.62    command; $undo$ does not apply.