--- a/doc-src/HOL/HOL.tex Mon Mar 13 16:23:34 2000 +0100
+++ b/doc-src/HOL/HOL.tex Mon Mar 13 16:24:23 2000 +0100
@@ -439,9 +439,9 @@
\item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI}
repeatedly to remove all outermost universal quantifiers and implications
from subgoal $i$.
-\item[\ttindexbold{cases_tac} {\tt"}$P${\tt"} $i$] performs case distinction
- on $P$ for subgoal $i$: the latter is replaced by two identical subgoals
- with the added assumptions $P$ and $\lnot P$, respectively.
+\item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on
+ $P$ for subgoal $i$: the latter is replaced by two identical subgoals with
+ the added assumptions $P$ and $\lnot P$, respectively.
\item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then
\texttt{mp} in subgoal $i$, which is typically useful when forward-chaining
from an induction hypothesis. As a generalization of \texttt{mp_tac},
@@ -2198,7 +2198,7 @@
In some cases, induction is overkill and a case distinction over all
constructors of the datatype suffices.
\begin{ttdescription}
-\item[\ttindexbold{cases_tac} {\tt"}$u${\tt"} $i$]
+\item[\ttindexbold{case_tac} {\tt"}$u${\tt"} $i$]
performs a case analysis for the term $u$ whose type must be a datatype.
If the datatype has $k@j$ constructors $C^j@1$, \dots $C^j@{k@j}$, subgoal
$i$ is replaced by $k@j$ new subgoals which contain the additional
@@ -2242,7 +2242,7 @@
For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt
+}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section,
but by more primitive means using \texttt{typedef}. To be able to use the
-tactics \texttt{induct_tac} and \texttt{cases_tac} and to define functions by
+tactics \texttt{induct_tac} and \texttt{case_tac} and to define functions by
primitive recursion on these types, such types may be represented as actual
datatypes. This is done by specifying an induction rule, as well as theorems
stating the distinctness and injectivity of constructors in a {\tt