author wenzelm Fri, 17 Mar 2000 22:50:41 +0100 changeset 8507 d22fcea34cb7 parent 8506 e2204e3df61b child 8508 76d8d8aab881
untag: only name arg; fixed trans att syntax; tuned case command;
--- 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.