doc-src/HOL/HOL.tex

changeset 6620 | fc991461c7b9 |

parent 6592 | c120262044b6 |

child 6626 | a92d2b6e0626 |

--- 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