Inf/Sup now purely syntactic
authorhaftmann
Wed, 07 Oct 2009 09:44:03 +0200
changeset 32885 5cab25b2dcf9
parent 32884 a0737458da18
child 32886 aba29da80c1b
Inf/Sup now purely syntactic
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}