changeset 14202 | 643fc73e2910 |
parent 14158 | 15bab630ae31 |
child 28871 | 111bbd2b12db |
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