--- a/doc-src/Main/Docs/Main_Doc.thy Sat Feb 06 00:22:01 2010 +0100
+++ b/doc-src/Main/Docs/Main_Doc.thy Sat Feb 06 08:42:37 2010 +0100
@@ -48,8 +48,8 @@
\smallskip
\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
-@{const HOL.less_eq} & @{typeof HOL.less_eq} & (\verb$<=$)\\
-@{const HOL.less} & @{typeof HOL.less}\\
+@{const Algebras.less_eq} & @{typeof Algebras.less_eq} & (\verb$<=$)\\
+@{const Algebras.less} & @{typeof Algebras.less}\\
@{const Orderings.Least} & @{typeof Orderings.Least}\\
@{const Orderings.min} & @{typeof Orderings.min}\\
@{const Orderings.max} & @{typeof Orderings.max}\\