--- a/doc-src/Main/Docs/Main_Doc.thy Wed Jan 12 21:49:04 2011 +0100
+++ b/doc-src/Main/Docs/Main_Doc.thy Wed Jan 12 21:57:01 2011 +0100
@@ -475,7 +475,8 @@
\begin{tabular}{@ {} l @ {~::~} l @ {}}
@{const Option.the} & @{typeof Option.the}\\
@{const Option.map} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
-@{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}
+@{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}\\
+@{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"}
\end{tabular}
\section{List}
--- a/doc-src/Main/Docs/document/Main_Doc.tex Wed Jan 12 21:49:04 2011 +0100
+++ b/doc-src/Main/Docs/document/Main_Doc.tex Wed Jan 12 21:57:01 2011 +0100
@@ -485,7 +485,8 @@
\begin{tabular}{@ {} l @ {~::~} l @ {}}
\isa{the} & \isa{{\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a}\\
\isa{Option{\isaliteral{2E}{\isachardot}}map} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{22}{\isachardoublequote}}}\\
-\isa{Option{\isaliteral{2E}{\isachardot}}set} & \isa{{\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}
+\isa{Option{\isaliteral{2E}{\isachardot}}set} & \isa{{\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set}\\
+\isa{Option{\isaliteral{2E}{\isachardot}}bind} & \isa{{\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ option}
\end{tabular}
\section{List}