# HG changeset patch
# User wenzelm
# Date 1316350527 -7200
# Node ID c56a400592580e4b2ca79e71e1ee69f63fec2e4b
# Parent  52744e1444322fc9803d68b8fea4a61d3a781010
updated Complete_Lattices;

diff -r 52744e144432 -r c56a40059258 doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Sun Sep 18 14:48:25 2011 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Sun Sep 18 14:55:27 2011 +0200
@@ -82,8 +82,8 @@
 \begin{tabular}{@ {} l @ {~::~} l @ {}}
 @{const Lattices.inf} & @{typeof Lattices.inf}\\
 @{const Lattices.sup} & @{typeof Lattices.sup}\\
-@{const Complete_Lattice.Inf} & @{term_type_only Complete_Lattice.Inf "'a set \<Rightarrow> 'a::Inf"}\\
-@{const Complete_Lattice.Sup} & @{term_type_only Complete_Lattice.Sup "'a set \<Rightarrow> 'a::Sup"}\\
+@{const Complete_Lattices.Inf} & @{term_type_only Complete_Lattices.Inf "'a set \<Rightarrow> 'a::Inf"}\\
+@{const Complete_Lattices.Sup} & @{term_type_only Complete_Lattices.Sup "'a set \<Rightarrow> 'a::Sup"}\\
 \end{tabular}
 
 \subsubsection*{Syntax}