--- 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}
%(*