# HG changeset patch
# User haftmann
# Date 1606636670 0
# Node ID 4dcd05a26795d949a747abab046bc7fb86c1b42b
# Parent  4ab04bafae356e3919e3474c592cd8c86fff4394
typo

diff -r 4ab04bafae35 -r 4dcd05a26795 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sat Nov 28 21:38:48 2020 +0000
+++ b/src/Doc/System/Sessions.thy	Sun Nov 29 07:57:50 2020 +0000
@@ -151,7 +151,7 @@
   \<^descr> \isakeyword{document_theories}~\<open>names\<close> specifies theories from other
   sessions that should be included in the generated document source directory.
   These theories need to be explicit imports in the current session, or
-  impliciti imports from the underlying hierarchy of parent sessions. The
+  implicit imports from the underlying hierarchy of parent sessions. The
   generated \<^verbatim>\<open>session.tex\<close> file is not affected: the session's {\LaTeX} setup
   needs to \<^verbatim>\<open>\input{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> generated \<^verbatim>\<open>.tex\<close> files separately.