doc-src/TutorialI/Types/numerics.tex

--- a/doc-src/TutorialI/Types/numerics.tex	Wed Aug 08 14:33:10 2001 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex	Wed Aug 08 14:50:28 2001 +0200
@@ -225,7 +225,7 @@
 \rulename{nat_diff_split}
 \end{isabelle}
 For example, it proves the following fact, which lies outside the scope of
-linear arithmetic:
+linear arithmetic:\REMARK{replace by new example!}
 \begin{isabelle}
 \isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline
 \isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline