1.1 --- a/doc-src/TutorialI/Misc/pairs.thy	Fri Sep 01 18:29:52 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/pairs.thy	Fri Sep 01 19:09:44 2000 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  text{*
     1.5  HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
     1.6    $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
     1.7 -are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and
     1.8 +are extracted by @{term"fst"} and @{term"snd"}: \isa{fst($x$,$y$) = $x$} and
     1.9  \isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
    1.10  \isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and
    1.11  \isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ *