--- a/doc-src/Main/Docs/Main_Doc.thy Tue Oct 20 13:37:56 2009 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy Tue Oct 20 14:44:02 2009 +0200
@@ -164,6 +164,21 @@
\end{tabular}
+\section{Hilbert\_Choice}
+
+Hilbert's selection ($\varepsilon$) operator: @{term"SOME x. P"}.
+\smallskip
+
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
+@{const Hilbert_Choice.inv_onto} & @{term_type_only Hilbert_Choice.inv_onto "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"}
+\end{tabular}
+
+\subsubsection*{Syntax}
+
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+@{term inv} & @{term[source]"inv_onto UNIV"}
+\end{tabular}
+
\section{Fixed Points}
Theory: @{theory Inductive}.