# HG changeset patch
# User haftmann
# Date 1254901443 -7200
# Node ID 5cab25b2dcf98149dbf48d18337d6ad45ffa7173
# Parent  a0737458da18e2a133d5c68d1b03899554ff6f7e
Inf/Sup now purely syntactic

diff -r a0737458da18 -r 5cab25b2dcf9 doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Tue Oct 06 20:19:54 2009 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Wed Oct 07 09:44:03 2009 +0200
@@ -79,8 +79,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::complete_lattice"}\\
-@{const Complete_Lattice.Sup} & @{term_type_only Complete_Lattice.Sup "'a set \<Rightarrow> 'a::complete_lattice"}\\
+@{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"}\\
 \end{tabular}
 
 \subsubsection*{Syntax}