diff -r a8b1a44d8264 -r 79f9fbef9106 doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Mon Jan 12 16:45:35 2004 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy	Mon Jan 12 16:51:45 2004 +0100
@@ -763,13 +763,13 @@
 *}
 
 lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x"
-  by (auto(*<*)simp add: int_less_le(*>*))
+  by (auto(*<*)simp add: zero_less_mult_iff(*>*))
 
 text {*
   \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}
 %(*