1.1 --- a/doc-src/ZF/ZF.tex	Tue Sep 23 15:42:01 2003 +0200
     1.2 +++ b/doc-src/ZF/ZF.tex	Tue Sep 23 15:44:25 2003 +0200
     1.3 @@ -1807,7 +1807,7 @@
     1.4  In some situations, induction is overkill and a case distinction over all
     1.5  constructors of the datatype suffices.
     1.6  \begin{ttdescription}
     1.7 -\item[\methdx{Inductive.case_tac} $x$]
     1.8 +\item[\methdx{case_tac} $x$]
     1.9   performs a case analysis for the variable~$x$.
    1.10  \end{ttdescription}
    1.11