--- a/src/Doc/System/Presentation.thy Sat Jan 06 22:55:52 2018 +0100
+++ b/src/Doc/System/Presentation.thy Sun Jan 07 11:12:34 2018 +0100
@@ -167,7 +167,7 @@
run.
\<^medskip>
- Option \<^verbatim>\<open>-d\<close> specifies an laternative document output directory. The default
+ Option \<^verbatim>\<open>-d\<close> specifies an alternative document output directory. The default
is \<^verbatim>\<open>output/document\<close> (derived from the document name). Note that the result
will appear in the parent of this directory.