# HG changeset patch
# User nipkow
# Date 1496135520 -7200
# Node ID 3de7464450b045c81b5457c8144f267923fc312d
# Parent  ca1e636fa7169b8586f89ca125ea53993a100a46
adjusted doc

diff -r ca1e636fa716 -r 3de7464450b0 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Tue May 30 10:03:35 2017 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Tue May 30 11:12:00 2017 +0200
@@ -61,9 +61,9 @@
 @{const Orderings.less_eq} & @{typeof Orderings.less_eq} & (\<^verbatim>\<open><=\<close>)\\
 @{const Orderings.less} & @{typeof Orderings.less}\\
 @{const Orderings.Least} & @{typeof Orderings.Least}\\
+@{const Orderings.Greatest} & @{typeof Orderings.Greatest}\\
 @{const Orderings.min} & @{typeof Orderings.min}\\
 @{const Orderings.max} & @{typeof Orderings.max}\\
-@{const Lattices_Big.arg_min} & @{typeof Lattices_Big.arg_min}\\
 @{const[source] top} & @{typeof Orderings.top}\\
 @{const[source] bot} & @{typeof Orderings.bot}\\
 @{const Orderings.mono} & @{typeof Orderings.mono}\\
@@ -79,6 +79,7 @@
 @{term "\<exists>x\<le>y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\
 \multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\
 @{term "LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\
+@{term "GREATEST x. P"} & @{term[source]"Greatest (\<lambda>x. P)"}\\
 \end{supertabular}
 
 
@@ -420,7 +421,6 @@
 @{const Lattices_Big.is_arg_min} & @{typeof Lattices_Big.is_arg_min}\\
 @{const Lattices_Big.arg_max} & @{typeof Lattices_Big.arg_max}\\
 @{const Lattices_Big.is_arg_max} & @{typeof Lattices_Big.is_arg_max}\\
-@{const Lattices_Big.Greatest} & @{typeof Lattices_Big.Greatest}\\
 \end{supertabular}
 
 \subsubsection*{Syntax}
@@ -428,7 +428,6 @@
 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
 @{term "ARG_MIN f x. P"} & @{term[source]"arg_min f (\<lambda>x. P)"}\\
 @{term "ARG_MAX f x. P"} & @{term[source]"arg_max f (\<lambda>x. P)"}\\
-@{term "GREATEST x. P"} & @{term[source]"Greatest (\<lambda>x. P)"}\\
 \end{supertabular}