# HG changeset patch
# User nipkow
# Date 861377606 -7200
# Node ID 3bb5d1b9c3aa2f943fd3a264201196c716bcc36e
# Parent  9e46778b97ab5689615a93ea7d5aee0a442037ab
Tuple patterns are allowed now in `case'

diff -r 9e46778b97ab -r 3bb5d1b9c3aa doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Fri Apr 18 16:54:52 1997 +0200
+++ b/doc-src/Logics/HOL.tex	Fri Apr 18 17:33:26 1997 +0200
@@ -952,6 +952,7 @@
 \S\ref{sec:HOL:datatype}.
 
 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
+\label{subsec:prod-sum}
 
 \begin{figure}[htbp]
 \begin{constants}
@@ -1576,10 +1577,12 @@
                            \mid & C_m~x_{m1}~\dots~x_{mk_m} & \To & e_m
 \end{array}
 \]
+where the $x_{ij}$ are either identifiers or nested tuple patterns as in
+\S\ref{subsec:prod-sum}.
 \begin{warn}
 In contrast to \ML, {\em all} constructors must be present, their order is
-fixed, and nested patterns are not supported. Violating this restriction
-results in strange error messages.
+fixed, and nested patterns are not supported (with the exception of tuples).
+Violating this restriction results in strange error messages.
 \end{warn}
 
 \underscoreoff