doc-src/TutorialI/Misc/simp.thy

--- a/doc-src/TutorialI/Misc/simp.thy	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy	Fri Jan 26 15:50:28 2001 +0100
@@ -162,7 +162,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