--- a/doc-src/TutorialI/Misc/Option2.thy Fri May 18 17:18:43 2001 +0200
+++ b/doc-src/TutorialI/Misc/Option2.thy Sat May 19 12:19:23 2001 +0200
@@ -11,7 +11,7 @@
datatype 'a option = None | Some 'a;
text{*\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 @{text"t option"} can model the result of a computation that
may either terminate with an error (represented by @{term None}) or return
some value @{term v} (represented by @{term"Some v"}).