case_tac tweak
authorpaulson
Tue, 23 Sep 2003 15:44:25 +0200
changeset 14202 643fc73e2910
parent 14201 7ad7ab89c402
child 14203 97df98601d23
case_tac tweak
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}