diff -r d666f11ca2d4 -r 51e70b7bc315 doc-src/TutorialI/Misc/document/Option2.tex --- a/doc-src/TutorialI/Misc/document/Option2.tex Fri May 18 17:18:43 2001 +0200 +++ b/doc-src/TutorialI/Misc/document/Option2.tex Sat May 19 12:19:23 2001 +0200 @@ -9,7 +9,7 @@ \isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a% \begin{isamarkuptext}% \noindent -Frequently one needs to add a distiguished element to some existing type. +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}).