doc-src/TutorialI/Documents/Documents.thy

   than they really were.  For example, this ``fully automatic'' proof
   is actually a fake:
 *}
 
 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}
 %(*
 
   \medskip Suppressing portions of printed text demands care.  You
   should not misrepresent the underlying theory development.  It is