author wenzelm Mon, 13 Mar 2000 16:24:23 +0100 changeset 8443 0ed4b608ba4b parent 8442 96023903c2df child 8444 8f8eb220d9aa
renamed cases_tac to case_tac;
 doc-src/HOL/HOL.tex file | annotate | diff | comparison | revisions
--- 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