--- 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}.