# HG changeset patch
# User krauss
# Date 1294865821 -3600
# Node ID 0d34deffb0e904e8b76135465ebeac3e0f8c754a
# Parent  a392a18676e960df43b336c32146d8372f687c9b
documented Option.bind

diff -r a392a18676e9 -r 0d34deffb0e9 doc-src/Main/Docs/Main_Doc.thy
--- 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}
diff -r a392a18676e9 -r 0d34deffb0e9 doc-src/Main/Docs/document/Main_Doc.tex
--- 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}