author paulson Tue Jan 23 11:10:39 1996 +0100 (1996-01-23) changeset 1448 77379ae9ff0d parent 1447 bc2c0acbbf29 child 1449 25a7ddf9c080
Stylistic changes to discussion of pattern-matching
 doc-src/Logics/HOL.tex file | annotate | diff | revisions
     1.1 --- a/doc-src/Logics/HOL.tex	Tue Jan 23 10:59:35 1996 +0100
1.2 +++ b/doc-src/Logics/HOL.tex	Tue Jan 23 11:10:39 1996 +0100
1.3 @@ -950,13 +950,7 @@
1.4  In addition, it is possible to use tuples
1.5  as patterns in abstractions:
1.6  \begin{center}
1.7 -\begin{tabular}{|c|c|}
1.8 -\hline
1.9 -external & internal \\
1.10 -\hline
1.11 -{\tt\%($x$,$y$).$t$} & {\tt split(\%$x$ $y$.$t$)} \\
1.12 -\hline
1.13 -\end{tabular}
1.14 +{\tt\%($x$,$y$).$t$} \quad stands for\quad {\tt split(\%$x$ $y$.$t$)}
1.15  \end{center}
1.16  Nested patterns are possible and are translated stepwise:
1.17  {\tt\%($x$,$y$,$z$).$t$} $\leadsto$ {\tt\%($x$,($y$,$z$)).$t$} $\leadsto$
1.18 @@ -964,10 +958,10 @@
1.19    $z$.$t$))}. The reverse translation is performed upon printing.
1.20  \begin{warn}
1.21    The translation between patterns and {\tt split} is performed automatically
1.22 -  by the parser and printer. This means that the internal and external form
1.23 -  of a term may differ, which has to be taken into account during the proof
1.24 -  process. For example the term {\tt (\%(x,y).(y,x))(a,b)} requires the
1.25 -  theorem {\tt split} to rewrite to {\tt(b,a)}.
1.26 +  by the parser and printer.  Thus the internal and external form of a term
1.27 +  may differ, whichs affects proofs.  For example the term {\tt
1.28 +    (\%(x,y).(y,x))(a,b)} requires the theorem {\tt split} to rewrite to
1.29 +  {\tt(b,a)}.
1.30  \end{warn}
1.31  In addition to explicit $\lambda$-abstractions, patterns can be used in any
1.32  variable binding construct which is internally described by a