diff -r d40cc6e7bfd8 -r aea72a834c85 doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Thu Nov 29 21:12:37 2001 +0100
@@ -45,6 +45,13 @@
   $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
   to include simplification rules that can lead to nontermination, either on
   their own or in combination with other simplification rules.
+\end{warn}
+\begin{warn}
+  It is inadvisable to toggle the simplification attribute of a
+  theorem from a \emph{parent} theory $A$ in a child theory $B$ for good.
+  The reason is that if some theory $C$ is based both on $B$ and (via a
+  differnt path) on $A$, it is not defined what the simplification attribute
+  of that theorem will be in $C$: it could be either.
 \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%