# HG changeset patch
# User haftmann
# Date 1265442142 -3600
# Node ID 8c339c73495c3b79cbe0bdd16e410edbdff2bf7d
# Parent  5312d2ffee3bef8bfa1b515a9cee6eaf3f5f4099
adjusted to changeset 118b41bba42b5

diff -r 5312d2ffee3b -r 8c339c73495c doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Thu Feb 04 14:45:08 2010 +0100
+++ b/doc-src/Main/Docs/Main_Doc.thy	Sat Feb 06 08:42:22 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}\\