diff -r f061129d891b -r 63d7aca15f6b src/Doc/System/Presentation.thy
--- 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.