--- a/doc-src/TutorialI/Misc/document/Option2.tex Thu Jul 26 16:54:44 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-%
-\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: