# 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%