# HG changeset patch
# User paulson
# Date 822391839 -3600
# Node ID 77379ae9ff0dc7b9be0cfac82805717c0d35caa8
# Parent  bc2c0acbbf29c17440240fbf82fd41a205bf42f7
Stylistic changes to discussion of pattern-matching

diff -r bc2c0acbbf29 -r 77379ae9ff0d doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Tue Jan 23 10:59:35 1996 +0100
+++ b/doc-src/Logics/HOL.tex	Tue Jan 23 11:10:39 1996 +0100
@@ -950,13 +950,7 @@
 In addition, it is possible to use tuples
 as patterns in abstractions:
 \begin{center}
-\begin{tabular}{|c|c|}
-\hline
-external & internal \\
-\hline
-{\tt\%($x$,$y$).$t$} & {\tt split(\%$x$ $y$.$t$)} \\
-\hline
-\end{tabular}
+{\tt\%($x$,$y$).$t$} \quad stands for\quad {\tt split(\%$x$ $y$.$t$)} 
 \end{center}
 Nested patterns are possible and are translated stepwise:
 {\tt\%($x$,$y$,$z$).$t$} $\leadsto$ {\tt\%($x$,($y$,$z$)).$t$} $\leadsto$
@@ -964,10 +958,10 @@
   $z$.$t$))}. The reverse translation is performed upon printing.
 \begin{warn}
   The translation between patterns and {\tt split} is performed automatically
-  by the parser and printer. This means that the internal and external form
-  of a term may differ, which has to be taken into account during the proof
-  process. For example the term {\tt (\%(x,y).(y,x))(a,b)} requires the
-  theorem {\tt split} to rewrite to {\tt(b,a)}.
+  by the parser and printer.  Thus the internal and external form of a term
+  may differ, whichs affects proofs.  For example the term {\tt
+    (\%(x,y).(y,x))(a,b)} requires the theorem {\tt split} to rewrite to
+  {\tt(b,a)}.
 \end{warn}
 In addition to explicit $\lambda$-abstractions, patterns can be used in any
 variable binding construct which is internally described by a