doc-src/TutorialI/Types/document/Pairs.tex
changeset 14387 e96d5c42c4b0
parent 13791 3b6ff7ceaf27
child 15446 b022b72ccc03
--- a/doc-src/TutorialI/Types/document/Pairs.tex	Sat Feb 14 02:06:12 2004 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex	Sun Feb 15 10:46:37 2004 +0100
@@ -33,7 +33,7 @@
 \isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y}\\
 \isa{{\isasymforall}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}A{\isachardot}\ x{\isacharequal}y}\\
 \isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharcomma}z{\isacharparenright}{\isachardot}\ x{\isacharequal}z{\isacharbraceright}}\\
-\isa{{\isasymUnion}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A{\isachardot}\ {\isacharbraceleft}x\ {\isacharplus}\ y{\isacharbraceright}}
+\isa{{\isasymUnion}\isactrlbsub {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A\isactrlesub \ {\isacharbraceleft}x\ {\isacharplus}\ y{\isacharbraceright}}
 \end{quote}
 The intuitive meanings of these expressions should be obvious.
 Unfortunately, we need to know in more detail what the notation really stands