doc-src/TutorialI/Types/numerics.tex

 0)\ \isasymand \ (\isasymforall d.\ a\ =\ b+d\ \isasymlongrightarrow \ P\
 d))
 \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
 \isacommand{done}
 \end{isabelle}