diff -r d40cc6e7bfd8 -r aea72a834c85 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Thu Nov 29 21:12:37 2001 +0100
@@ -61,6 +61,16 @@
 \item a basic repertoire of proof commands.
 \end{itemize}
 
+\begin{warn}
+It is tempting to think that all lemmas should have the \isa{simp} attribute
+just because this was the case in the example above. However, in that example
+all lemmas were equations, and the right-hand side was simpler than the
+left-hand side --- an ideal situation for simplification purposes. Unless
+this is clearly the case, novices should refrain from awarding a lemma the
+\isa{simp} attribute, which has a global effect. Instead, lemmas can be
+applied locally where they are needed, which is discussed in the following
+chapter.
+\end{warn}
 
 \section{Some Helpful Commands}
 \label{sec:commands-and-hints}
@@ -513,7 +523,6 @@
 \input{Recdef/document/examples.tex}
 
 \subsection{Proving Termination}
-
 \input{Recdef/document/termination.tex}
 
 \subsection{Simplification and Recursive Functions}