# HG changeset patch
# User wenzelm
# Date 1008961002 -3600
# Node ID cf5a342ce69831f648538a1b080edac946c7186d
# Parent  2fcf06f05afa69cfde2ed1297bc5389a4ed281b1
updated;

diff -r 2fcf06f05afa -r cf5a342ce698 doc-src/TutorialI/Misc/document/simp.tex
--- 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,