doc-src/TutorialI/Documents/Documents.thy

   image like \texttt{HOL}.  This results in an overall tree structure,
   which is reflected by the output location in the file system
   (usually rooted at \verb,~/isabelle/browser_info,).
 
   \medskip The easiest way to manage Isabelle sessions is via
-  \texttt{isatool mkdir} (generates an initial session source setup)
-  and \texttt{isatool make} (run sessions controlled by
+  \texttt{isabelle mkdir} (generates an initial session source setup)
+  and \texttt{isabelle make} (run sessions controlled by
   \texttt{IsaMakefile}).  For example, a new session
   \texttt{MySession} derived from \texttt{HOL} may be produced as
   follows:
 
 \begin{verbatim}
-  isatool mkdir HOL MySession
-  isatool make
+  isabelle mkdir HOL MySession
+  isabelle make
 \end{verbatim}
 
-  The \texttt{isatool make} job also informs about the file-system
+  The \texttt{isabelle make} job also informs about the file-system
   location of the ultimate results.  The above dry run should be able
   to produce some \texttt{document.pdf} (with dummy title, empty table
   of contents etc.).  Any failure at this stage usually indicates
   technical problems of the {\LaTeX} installation.
 

   \item \texttt{IsaMakefile} holds appropriate dependencies and
   invocations of Isabelle tools to control the batch job.  In fact,
   several sessions may be managed by the same \texttt{IsaMakefile}.
   See the \emph{Isabelle System Manual} \cite{isabelle-sys} 
   for further details, especially on
-  \texttt{isatool usedir} and \texttt{isatool make}.
+  \texttt{isabelle usedir} and \texttt{isabelle make}.
 
   \end{itemize}
 
   One may now start to populate the directory \texttt{MySession}, and
   the file \texttt{MySession/ROOT.ML} accordingly.  The file

 
   \medskip Any additional files for the {\LaTeX} stage go into the
   \texttt{MySession/document} directory as well.  In particular,
   adding a file named \texttt{root.bib} causes an automatic run of
   \texttt{bibtex} to process a bibliographic database; see also
-  \texttt{isatool document} \cite{isabelle-sys}.
+  \texttt{isabelle document} \cite{isabelle-sys}.
 
   \medskip Any failure of the document preparation phase in an
   Isabelle batch session leaves the generated sources in their target
   location, identified by the accompanying error message.  This lets
   you trace {\LaTeX} problems with the generated files at hand.

   same tag are joined into a single region.  The Isabelle document
   preparation system allows the user to specify how to interpret a
   tagged region, in order to keep, drop, or fold the corresponding
   parts of the document.  See the \emph{Isabelle System Manual}
   \cite{isabelle-sys} for further details, especially on
-  \texttt{isatool usedir} and \texttt{isatool document}.
+  \texttt{isabelle usedir} and \texttt{isabelle document}.
 
   Ignored material is specified by delimiting the original formal
   source with special source comments
   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
   \verb,(,\verb,*,\verb,>,\verb,*,\verb,),.  These parts are stripped