doc-src/ZF/ZF.tex

 % 
 % we also have the ind_cases method, but what does it do?
 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}
 
 Both tactics can only be applied to a variable, whose typing must be given in
 some assumption, for example the assumption \isa{x \isasymin \ list(A)}.  The tactics