doc-src/TutorialI/Types/document/Pairs.tex
changeset 15446 b022b72ccc03
parent 14387 e96d5c42c4b0
child 15481 fc075ae929e4
--- 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%