--- a/doc-src/TutorialI/Types/document/Pairs.tex Wed Jan 19 16:45:24 2005 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex Fri Jan 21 13:51:39 2005 +0100
@@ -131,7 +131,7 @@
\end{isabelle}
Again, simplification produces a term suitable for \isa{split{\isacharunderscore}split}
as above. If you are worried about the strange form of the premise:
-\isa{split\ op\ {\isacharequal}} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y}.
+\isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x\ {\isacharequal}\ y} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y}.
The same proof procedure works for%
\end{isamarkuptxt}%
\isamarkuptrue%