doc-src/HOL/HOL.tex

--- a/doc-src/HOL/HOL.tex	Mon May 10 15:17:14 1999 +0200
+++ b/doc-src/HOL/HOL.tex	Mon May 10 15:26:30 1999 +0200
@@ -242,7 +242,7 @@
 \end{warn}
 
 
-\subsection{The \sdx{let} and \sdx{case} constructions}
+\subsection{The let and case constructions}
 Local abbreviations can be introduced by a \texttt{let} construct whose
 syntax appears in Fig.\ts\ref{hol-grammar}.  Internally it is translated into
 the constant~\cdx{Let}.  It can be expanded by rewriting with its