# HG changeset patch
# User wenzelm
# Date 952961063 -3600
# Node ID 0ed4b608ba4bfa95239d458da0b28d83c2bd941c
# Parent  96023903c2df15670aa16d0011322d4b3007a881
renamed cases_tac to case_tac;

diff -r 96023903c2df -r 0ed4b608ba4b doc-src/HOL/HOL.tex
--- 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