diff -r 587c893049e1 -r f228929a6fab doc-src/Main/Docs/document/Main_Doc.tex
--- a/doc-src/Main/Docs/document/Main_Doc.tex	Mon Feb 22 09:30:50 2010 +0100
+++ b/doc-src/Main/Docs/document/Main_Doc.tex	Mon Feb 22 09:36:29 2010 +0100
@@ -416,7 +416,7 @@
 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
 \isa{{\isasymSum}A} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x{\isacharparenright}\ A{\isachardoublequote}} & (\verb$SUM$)\\
 \isa{{\isasymSum}x{\isasymin}A{\isachardot}\ t} & \isa{{\isachardoublequote}setsum\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ t{\isacharparenright}\ A{\isachardoublequote}}\\
-\isa{{\isachardoublequote}{\isasymSum}x{\isacharbar}P{\isachardot}\ t{\isachardoublequote}} & \isa{{\isasymSum}x{\isasymin}{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}{\isachardot}\ t}\\
+\isa{{\isachardoublequote}{\isasymSum}x{\isacharbar}P{\isachardot}\ t{\isachardoublequote}} & \isa{{\isasymSum}x\ {\isacharbar}\ P{\isachardot}\ t}\\
 \multicolumn{2}{@ {}l@ {}}{Similarly for \isa{{\isasymProd}} instead of \isa{{\isasymSum}}} & (\verb$PROD$)\\
 \end{supertabular}