author | paulson |
Tue, 23 Sep 2003 15:44:25 +0200 | |
changeset 14202 | 643fc73e2910 |
parent 14201 | 7ad7ab89c402 |
child 14203 | 97df98601d23 |
doc-src/ZF/ZF.tex | file | annotate | diff | comparison | revisions |
--- 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}