diff -r c1597167563e -r 9cde8c4ea5a5 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Thu Sep 12 13:39:04 2019 +0200
+++ b/src/Doc/System/Sessions.thy	Thu Sep 12 14:22:47 2019 +0200
@@ -484,92 +484,6 @@
 \<close>
 
 
-section \<open>Maintain theory imports wrt.\ session structure\<close>
-
-text \<open>
-  The @{tool_def "imports"} tool helps to maintain theory imports wrt.\
-  session structure. It supports three main operations via options \<^verbatim>\<open>-I\<close>,
-  \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-U\<close>. Its command-line usage is: @{verbatim [display]
-\<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...]
-
-  Options are:
-    -B NAME      include session NAME and all descendants
-    -D DIR       include session directory and select its sessions
-    -I           operation: report session imports
-    -M           operation: Mercurial repository check for theory files
-    -R           operate on requirements of selected sessions
-    -U           operation: update theory imports to use session qualifiers
-    -X NAME      exclude sessions from group NAME and all descendants
-    -a           select all sessions
-    -d DIR       include session directory
-    -g NAME      select session group NAME
-    -i           incremental update according to session graph structure
-    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
-    -v           verbose
-    -x NAME      exclude session NAME and all descendants
-
-  Maintain theory imports wrt. session structure. At least one operation
-  needs to be specified (see options -I -M -U).\<close>}
-
-  \<^medskip>
-  The selection of sessions and session directories works as for @{tool build}
-  via options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> (see
-  \secref{sec:tool-build}).
-
-  \<^medskip>
-  Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
-  (see \secref{sec:tool-build}).
-
-  \<^medskip>
-  Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
-
-  \<^medskip>
-  Option \<^verbatim>\<open>-I\<close> determines reports session imports:
-
-    \<^descr>[Potential session imports] are derived from old-style use of theory
-    files from other sessions via the directory structure. After declaring
-    those as \isakeyword{sessions} in the corresponding \<^verbatim>\<open>ROOT\<close> file entry, a
-    proper session-qualified theory name can be used (cf.\ option \<^verbatim>\<open>-U\<close>). For
-    example, adhoc \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"~~/src/HOL/Library/Multiset"\<close> becomes formal
-    \<^theory_text>\<open>imports\<close> \<^verbatim>\<open>"HOL-Library.Multiset"\<close> after adding \isakeyword{sessions}
-    \<^verbatim>\<open>"HOL-Library"\<close> to the \<^verbatim>\<open>ROOT\<close> entry.
-
-    \<^descr>[Actual session imports] are derived from the session qualifiers of all
-    currently imported theories. This helps to minimize dependencies in the
-    session import structure to what is actually required.
-
-  \<^medskip>
-  Option \<^verbatim>\<open>-M\<close> checks imported theories against the Mercurial repositories of
-  the underlying session directories; non-repository directories are ignored.
-  This helps to find files that are accidentally ignored, e.g.\ due to
-  rearrangements of the session structure.
-
-  \<^medskip>
-  Option \<^verbatim>\<open>-U\<close> updates theory imports with old-style directory specifications
-  to canonical session-qualified theory names, according to the theory name
-  space imported via \isakeyword{sessions} within the \<^verbatim>\<open>ROOT\<close> specification.
-
-  Option \<^verbatim>\<open>-i\<close> modifies the meaning of option \<^verbatim>\<open>-U\<close> to proceed incrementally,
-  following to the session graph structure in bottom-up order. This may
-  lead to more accurate results in complex session hierarchies.
-\<close>
-
-subsubsection \<open>Examples\<close>
-
-text \<open>
-  Determine potential session imports for some project directory:
-  @{verbatim [display] \<open>isabelle imports -I -D 'some/where/My_Project'\<close>}
-
-  \<^smallskip>
-  Mercurial repository check for some project directory:
-  @{verbatim [display] \<open>isabelle imports -M -D 'some/where/My_Project'\<close>}
-
-  \<^smallskip>
-  Incremental update of theory imports for some project directory:
-  @{verbatim [display] \<open>isabelle imports -U -i -D 'some/where/My_Project'\<close>}
-\<close>
-
-
 section \<open>Retrieve theory exports \label{sec:tool-export}\<close>
 
 text \<open>