# HG changeset patch
# User haftmann
# Date 1266827789 -3600
# Node ID f228929a6fab2a374e040e0b19512bb5476b38f1
# Parent  587c893049e1d2b4d2b56ab0e4e6b9a4f35af02a
adjusted to cs. 8dfd816713c6

diff -r 587c893049e1 -r f228929a6fab doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Mon Feb 22 09:30:50 2010 +0100
+++ b/doc-src/Main/Docs/Main_Doc.thy	Mon Feb 22 09:36:29 2010 +0100
@@ -48,8 +48,8 @@
 \smallskip
 
 \begin{supertabular}{@ {} l @ {~::~} l l @ {}}
-@{const Algebras.less_eq} & @{typeof Algebras.less_eq} & (\verb$<=$)\\
-@{const Algebras.less} & @{typeof Algebras.less}\\
+@{const Orderings.less_eq} & @{typeof Orderings.less_eq} & (\verb$<=$)\\
+@{const Orderings.less} & @{typeof Orderings.less}\\
 @{const Orderings.Least} & @{typeof Orderings.Least}\\
 @{const Orderings.min} & @{typeof Orderings.min}\\
 @{const Orderings.max} & @{typeof Orderings.max}\\
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}