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

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