doc-src/System/Thy/Basics.thy

   \medskip The Isabelle system environment emerges from a few general
   concepts.
 
   \begin{itemize}
 
-  \item The \emph{Isabelle settings mechanism} provides environment variables to
-  all Isabelle programs (including tools and user interfaces).
+  \item The \emph{Isabelle settings mechanism} provides environment
+  variables to all Isabelle programs (including tools and user
+  interfaces).
 
   \item The \emph{Isabelle tools wrapper} (@{executable_def isatool})
   provides a generic startup platform for Isabelle related utilities.
   Thus tools automatically benefit from the settings mechanism.
 

 
 section {* The Isabelle tools wrapper \label{sec:isatool} *}
 
 text {*
   All Isabelle related utilities are called via a common wrapper ---
-  \ttindex{isatool}:
+  @{executable isatool}:
 
 \begin{ttbox}
 Usage: isatool TOOL [ARGS ...]
 
   Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL

   slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to
   refer to the current directory).
 *}
 
 
-subsection {* Options *}
+subsubsection {* Options *}
 
 text {*
   If the input heap file does not have write permission bits set, or
   the @{verbatim "-r"} option is given explicitely, then the session
   started will be read-only.  That is, the ML world cannot be

   may happen when errorneous ML code is provided. Also make sure that
   the ML commands are terminated properly by semicolon.
 
   \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
   "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
-  The @{verbatim "-f"} option passes ``@{verbatim "Session.finish ();"}'',
-  which is intended mainly for administrative purposes.
+  The @{verbatim "-f"} option passes ``@{verbatim
+  "Session.finish();"}'', which is intended mainly for administrative
+  purposes.
 
   \medskip The @{verbatim "-m"} option adds identifiers of print modes
   to be made active for this session. Typically, this is used by some
   user interface, e.g.\ to enable output of proper mathematical
   symbols.

   secure by disabling some critical operations, notably runtime
   compilation and evaluation of ML source code.
 *}
 
 
-subsection {* Examples *}
+subsubsection {* Examples *}
 
 text {*
   Run an interactive session of the default object-logic (as specified
   by the @{setting ISABELLE_LOGIC} setting) like this:
 \begin{ttbox}