diff -r a8b1a44d8264 -r 79f9fbef9106 doc-src/TutorialI/Documents/document/Documents.tex
--- a/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 12 16:45:35 2004 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Jan 12 16:51:45 2004 +0100
@@ -799,7 +799,7 @@
 \noindent Here the real source of the proof has been as follows:
 
 \begin{verbatim}
-  by (auto(*<*)simp add: int_less_le(*>*))
+  by (auto(*<*)simp add: zero_less_mult_iff(*>*))
 \end{verbatim}
 %(*