--- a/src/Doc/Main/Main_Doc.thy Sat May 27 22:52:08 2017 +0200
+++ b/src/Doc/Main/Main_Doc.thy Sun May 28 08:07:40 2017 +0200
@@ -63,6 +63,7 @@
@{const Orderings.Least} & @{typeof Orderings.Least}\\
@{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}\\
@@ -78,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 "ARG_MIN f x. P"} & @{term[source]"arg_min f (\<lambda>x. P)"}\\
\end{supertabular}
@@ -410,6 +412,21 @@
\end{supertabular}
+\section*{Lattices\_Big}
+
+\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
+@{const Lattices_Big.Min} & @{typeof Lattices_Big.Min}\\
+@{const Lattices_Big.Max} & @{typeof Lattices_Big.Max}\\
+@{const Lattices_Big.arg_min} & @{typeof Lattices_Big.arg_min}\\
+\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)"}\\
+\end{supertabular}
+
+
\section*{Groups\_Big}
\begin{supertabular}{@ {} l @ {~::~} l @ {}}