doc-src/Logics/HOL.tex
changeset 1448 77379ae9ff0d
parent 1429 1f0009009219
child 1471 b088c0a1f2bd
     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