author wenzelm Fri, 21 Dec 2001 19:56:42 +0100 changeset 12584 cf5a342ce698 parent 12583 2fcf06f05afa child 12585 e3cb192aa6ee
updated;
--- a/doc-src/TutorialI/Misc/document/simp.tex	Fri Dec 21 19:56:19 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Fri Dec 21 19:56:42 2001 +0100
@@ -181,8 +181,7 @@
Constant definitions (\S\ref{sec:ConstDefinitions}) can be used as
simplification rules, but by default they are not: the simplifier does not
expand them automatically.  Definitions are intended for introducing abstract
-concepts and not merely as abbreviations.  (Contrast with syntax
-translations, \S\ref{sec:def-translations}.)  Of course, we need to expand
+concepts and not merely as abbreviations.  Of course, we need to expand
the definition initially, but once we have proved enough abstract properties
of the new constant, we can forget its original definition.  This style makes
proofs more robust: if the definition has to be changed,