--- a/doc-src/TutorialI/Misc/pairs.thy Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Misc/pairs.thy Tue Sep 12 15:43:15 2000 +0200
@@ -2,13 +2,14 @@
theory pairs = Main:;
(*>*)
text{*
-HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
- $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
-are extracted by @{term"fst"} and @{term"snd"}: \isa{fst($x$,$y$) = $x$} and
-\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
-\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and
-\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ *
- $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
+HOL also has pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
+\indexboldpos{\isasymtimes}{$IsaFun} $\tau@2$ provided each $a@i$ is of type
+$\tau@i$. The components of a pair are extracted by @{term"fst"} and
+@{term"snd"}: \isa{fst($x$,$y$) = $x$} and \isa{snd($x$,$y$) = $y$}. Tuples
+are simulated by pairs nested to the right: \isa{($a@1$,$a@2$,$a@3$)} stands
+for \isa{($a@1$,($a@2$,$a@3$))} and $\tau@1 \times \tau@2 \times \tau@3$ for
+$\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have
+\isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.
It is possible to use (nested) tuples as patterns in abstractions, for
example \isa{\isasymlambda(x,y,z).x+y+z} and