diff -r 440fe0937b92 -r 431024edc9cf src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Sun May 28 11:32:15 2017 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Sun May 28 13:57:43 2017 +0200
@@ -79,7 +79,6 @@
 @{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 "ARG_MIN f x. P"} & @{term[source]"arg_min f (\<lambda>x. P)"}\\
 \end{supertabular}
 
 
@@ -419,12 +418,17 @@
 @{const Lattices_Big.Max} & @{typeof Lattices_Big.Max}\\
 @{const Lattices_Big.arg_min} & @{typeof Lattices_Big.arg_min}\\
 @{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}
 
 \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}