doc-src/ZF/ZF.tex

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