summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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

--- 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