# HG changeset patch
# User paulson
# Date 1106311899 -3600
# Node ID b022b72ccc03108a5b1449e41181cac42301eac5
# Parent  8244894d0a4141fa9a953cdd2fcef827a84715b6
auto update

diff -r 8244894d0a41 -r b022b72ccc03 doc-src/TutorialI/Types/document/Pairs.tex
--- 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%