--- a/doc-src/TutorialI/Types/document/Pairs.tex Fri Feb 16 08:10:28 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex Fri Feb 16 08:27:17 2001 +0100
@@ -9,7 +9,7 @@
\label{sec:products}
Pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
repertoire of operations: pairing and the two projections \isa{fst} and
-\isa{snd}. In any nontrivial application of pairs you will find that this
+\isa{snd}. In any non-trivial application of pairs you will find that this
quickly leads to unreadable formulae involvings nests of projections. This
section is concerned with introducing some syntactic sugar to overcome this
problem: pattern matching with tuples.%
@@ -30,10 +30,7 @@
\isa{{\isasymforall}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}A{\isachardot}\ x{\isacharequal}y}\\
\isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharcomma}z{\isacharparenright}{\isachardot}\ x{\isacharequal}z{\isacharbraceright}}\\
\isa{{\isasymUnion}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A{\isachardot}\ {\isacharbraceleft}x\ {\isacharplus}\ y{\isacharbraceright}}
-\end{quote}%
-\end{isamarkuptext}%
-%
-\begin{isamarkuptext}%
+\end{quote}
The intuitive meanings of these expressions should be obvious.
Unfortunately, we need to know in more detail what the notation really stands
for once we have to reason about it. Abstraction
@@ -66,7 +63,7 @@
\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}split{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptext}%
This works well if rewriting with \isa{split{\isacharunderscore}def} finishes the
-proof, as it does above. But if it doesn't, you end up with exactly what
+proof, as it does above. But if it does not, you end up with exactly what
we are trying to avoid: nests of \isa{fst} and \isa{snd}. Thus this
approach is neither elegant nor very practical in large examples, although it
can be effective in small ones.