author nipkow Tue, 20 Oct 2009 14:44:02 +0200 changeset 33019 bcf56a64ce1a parent 33015 575bd6548df9 child 33020 0908ed080ccf
--- 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}.