--- a/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 26 15:50:28 2001 +0100
@@ -166,7 +166,7 @@
Of course we can also unfold definitions in the middle of a proof.
You should normally not turn a definition permanently into a simplification
-rule because this defeats the whole purpose of an abbreviation.
+rule because this defeats the whole purpose.
\begin{warn}
If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold