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}\\