diff -r 619531d87ce4 -r 4e2ee88276d2 doc-src/TutorialI/document/Option2.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/Option2.tex	Thu Jul 26 19:59:06 2012 +0200
@@ -0,0 +1,56 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Option{\isadigit{2}}}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\begin{isamarkuptext}%
+\indexbold{*option (type)}\indexbold{*None (constant)}%
+\indexbold{*Some (constant)}
+Our final datatype is very simple but still eminently useful:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ {\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{3D}{\isacharequal}}\ None\ {\isaliteral{7C}{\isacharbar}}\ Some\ {\isaliteral{27}{\isacharprime}}a%
+\begin{isamarkuptext}%
+\noindent
+Frequently one needs to add a distinguished element to some existing type.
+For example, type \isa{t\ option} can model the result of a computation that
+may either terminate with an error (represented by \isa{None}) or return
+some value \isa{v} (represented by \isa{Some\ v}).
+Similarly, \isa{nat} extended with $\infty$ can be modeled by type
+\isa{nat\ option}. In both cases one could define a new datatype with
+customized constructors like \isa{Error} and \isa{Infinity},
+but it is often simpler to use \isa{option}. For an application see
+\S\ref{sec:Trie}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: