--- 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}.
--- a/doc-src/Main/Docs/document/Main_Doc.tex Tue Oct 20 13:37:56 2009 +0200
+++ b/doc-src/Main/Docs/document/Main_Doc.tex Tue Oct 20 14:44:02 2009 +0200
@@ -175,6 +175,21 @@
\end{tabular}
+\section{Hilbert\_Choice}
+
+Hilbert's selection ($\varepsilon$) operator: \isa{SOME\ x{\isachardot}\ P}.
+\smallskip
+
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
+\isa{inv{\isacharunderscore}onto} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a}
+\end{tabular}
+
+\subsubsection*{Syntax}
+
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+\isa{inv} & \isa{{\isachardoublequote}inv{\isacharunderscore}onto\ UNIV{\isachardoublequote}}
+\end{tabular}
+
\section{Fixed Points}
Theory: \isa{Inductive}.