author paulson Tue, 23 Jan 1996 11:10:39 +0100 changeset 1448 77379ae9ff0d parent 1447 bc2c0acbbf29 child 1449 25a7ddf9c080
Stylistic changes to discussion of pattern-matching
 doc-src/Logics/HOL.tex file | annotate | diff | comparison | revisions
--- 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