--- 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}).