# HG changeset patch
# User nipkow
# Date 1256042642 -7200
# Node ID bcf56a64ce1a5ec24270050009ad8d212015b4f7
# Parent  575bd6548df9d86244c1d9a2252ef22b8c31cb93
added Hilbert_Choice section

diff -r 575bd6548df9 -r bcf56a64ce1a doc-src/Main/Docs/Main_Doc.thy
--- 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}.
diff -r 575bd6548df9 -r bcf56a64ce1a doc-src/Main/Docs/document/Main_Doc.tex
--- 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}.