src/Doc/System/Sessions.thy
changeset 72769 4dcd05a26795
parent 72648 1cbac4ae934d
child 72876 626fcaebd049
--- 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.