updated generated file;
authorwenzelm
Sat Oct 04 17:40:58 2008 +0200 (2008-10-04)
changeset 28505f98751bd715f
parent 28504 7ad7d7d6df47
child 28506 3ab515ee4e6f
updated generated file;
doc-src/IsarRef/Thy/document/Document_Preparation.tex
doc-src/IsarRef/Thy/document/Introduction.tex
doc-src/System/Thy/document/Basics.tex
doc-src/System/Thy/document/Misc.tex
doc-src/System/Thy/document/Presentation.tex
     1.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Sat Oct 04 17:40:56 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Sat Oct 04 17:40:58 2008 +0200
     1.3 @@ -36,10 +36,10 @@
     1.4    easy by using the Isabelle \verb|mkdir| and \verb|make|
     1.5    tools.  First invoke
     1.6  \begin{ttbox}
     1.7 -  isatool mkdir Foo
     1.8 +  isabelle mkdir Foo
     1.9  \end{ttbox}
    1.10    to initialize a separate directory for session \verb|Foo| ---
    1.11 -  it is safe to experiment, since \verb|isatool mkdir| never
    1.12 +  it is safe to experiment, since \verb|isabelle mkdir| never
    1.13    overwrites existing files.  Ensure that \verb|Foo/ROOT.ML|
    1.14    holds ML commands to load all theories required for this session;
    1.15    furthermore \verb|Foo/document/root.tex| should include any
    1.16 @@ -51,7 +51,7 @@
    1.17    one level up from the \verb|Foo| directory location.  Now
    1.18    invoke
    1.19  \begin{ttbox}
    1.20 -  isatool make Foo
    1.21 +  isabelle make Foo
    1.22  \end{ttbox}
    1.23    to run the \verb|Foo| session, with browser information and
    1.24    document preparation enabled.  Unless any errors are reported by
     2.1 --- a/doc-src/IsarRef/Thy/document/Introduction.tex	Sat Oct 04 17:40:56 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Introduction.tex	Sat Oct 04 17:40:58 2008 +0200
     2.3 @@ -105,7 +105,7 @@
     2.4    the Isar interaction loop, with some support for command line
     2.5    editing.  For example:
     2.6  \begin{ttbox}
     2.7 -isatool tty\medskip
     2.8 +isabelle tty\medskip
     2.9  {\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip
    2.10  theory Foo imports Main begin;
    2.11  definition foo :: nat where "foo == 1";
     3.1 --- a/doc-src/System/Thy/document/Basics.tex	Sat Oct 04 17:40:56 2008 +0200
     3.2 +++ b/doc-src/System/Thy/document/Basics.tex	Sat Oct 04 17:40:58 2008 +0200
     3.3 @@ -40,21 +40,19 @@
     3.4    variables to all Isabelle programs (including tools and user
     3.5    interfaces).
     3.6  
     3.7 -  \item The \emph{raw Isabelle process} (\indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} or
     3.8 -  \indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}) runs logic sessions either
     3.9 -  interactively or in batch mode.  In particular, this view abstracts
    3.10 -  over the invocation of the actual ML system to be used.  Regular
    3.11 -  users rarely need to care about the low-level process.
    3.12 +  \item The \emph{raw Isabelle process} (\indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}) runs logic sessions either interactively or in
    3.13 +  batch mode.  In particular, this view abstracts over the invocation
    3.14 +  of the actual ML system to be used.  Regular users rarely need to
    3.15 +  care about the low-level process.
    3.16  
    3.17 -  \item The \emph{Isabelle tools wrapper} (\indexref{}{executable}{isatool}\hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}})
    3.18 +  \item The \emph{Isabelle tools wrapper} (\indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}})
    3.19    provides a generic startup environment Isabelle related utilities,
    3.20    user interfaces etc.  Such tools automatically benefit from the
    3.21    settings mechanism.
    3.22  
    3.23 -  \item The \emph{Isabelle interface wrapper} (\indexref{}{executable}{Isabelle}\hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}} or \indexref{}{executable}{isabelle-interface}\hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}}) provides some
    3.24 -  abstraction over the actual user interface to be used.  The de-facto
    3.25 -  standard interface for Isabelle is Proof~General
    3.26 -  \cite{proofgeneral}.
    3.27 +  \item The \emph{Isabelle interface wrapper} (\indexref{}{executable}{isabelle-interface}\hyperlink{executable.isabelle-interface}{\mbox{\isa{\isatt{isabelle{\isacharminus}interface}}}}) provides some abstraction over the actual
    3.28 +  user interface to be used.  The de-facto standard interface for
    3.29 +  Isabelle is Proof~General \cite{proofgeneral}.
    3.30  
    3.31    \end{enumerate}%
    3.32  \end{isamarkuptext}%
    3.33 @@ -144,7 +142,7 @@
    3.34    \begin{itemize}
    3.35  
    3.36    \item \indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PROCESS}}}}} and \indexdef{}{setting}{ISABELLE\_TOOL}\hypertarget{setting.ISABELLE-TOOL}{\hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOL}}}}} are set
    3.37 -  automatically to the absolute path names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} executables,
    3.38 +  automatically to the absolute path names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} executables,
    3.39    respectively.
    3.40    
    3.41    \item \indexref{}{setting}{ISABELLE\_OUTPUT}\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}} will have the identifiers of
    3.42 @@ -186,7 +184,7 @@
    3.43    a private \verb|$ISABELLE_HOME_USER/etc/settings|.
    3.44    
    3.45    \item[\indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PROCESS}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}, \hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOL}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] are automatically set to the full path
    3.46 -  names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} executables, respectively.  Thus other tools and scripts
    3.47 +  names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} and \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} executables, respectively.  Thus other tools and scripts
    3.48    need not assume that the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} directory is
    3.49    on the current search path of the shell.
    3.50    
    3.51 @@ -241,8 +239,8 @@
    3.52    document preparation (see also \secref{sec:tool-latex}).
    3.53    
    3.54    \item[\indexdef{}{setting}{ISABELLE\_TOOLS}\hypertarget{setting.ISABELLE-TOOLS}{\hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOLS}}}}}] is a colon separated list of
    3.55 -  directories that are scanned by \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} for external
    3.56 -  utility programs (see also \secref{sec:isatool}).
    3.57 +  directories that are scanned by \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} for external
    3.58 +  utility programs (see also \secref{sec:isabelle-tool}).
    3.59    
    3.60    \item[\indexdef{}{setting}{ISABELLE\_DOCS}\hypertarget{setting.ISABELLE-DOCS}{\hyperlink{setting.ISABELLE-DOCS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}DOCS}}}}}] is a colon separated list of
    3.61    directories with documentation files.
    3.62 @@ -277,10 +275,10 @@
    3.63  \isamarkuptrue%
    3.64  %
    3.65  \begin{isamarkuptext}%
    3.66 -The \indexdef{}{executable}{isabelle}\hypertarget{executable.isabelle}{\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}} (or \indexdef{}{executable}{isabelle-process}\hypertarget{executable.isabelle-process}{\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}}) executable runs bare-bones Isabelle logic
    3.67 -  sessions --- either interactively or in batch mode.  It provides an
    3.68 -  abstraction over the underlying ML system, and over the actual heap
    3.69 -  file locations.  Its usage is:
    3.70 +The \indexdef{}{executable}{isabelle-process}\hypertarget{executable.isabelle-process}{\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}} executable runs bare-bones
    3.71 +  Isabelle logic sessions --- either interactively or in batch mode.
    3.72 +  It provides an abstraction over the underlying ML system, and over
    3.73 +  the actual heap file locations.  Its usage is:
    3.74  
    3.75  \begin{ttbox}
    3.76  Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
    3.77 @@ -438,16 +436,16 @@
    3.78  \end{isamarkuptext}%
    3.79  \isamarkuptrue%
    3.80  %
    3.81 -\isamarkupsection{The Isabelle tools wrapper \label{sec:isatool}%
    3.82 +\isamarkupsection{The Isabelle tools wrapper \label{sec:isabelle-tool}%
    3.83  }
    3.84  \isamarkuptrue%
    3.85  %
    3.86  \begin{isamarkuptext}%
    3.87  All Isabelle related tools and interfaces are called via a common
    3.88 -  wrapper --- \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}}:
    3.89 +  wrapper --- \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}:
    3.90  
    3.91  \begin{ttbox}
    3.92 -Usage: isatool TOOL [ARGS ...]
    3.93 +Usage: isabelle TOOL [ARGS ...]
    3.94  
    3.95    Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
    3.96    for more specific help.
    3.97 @@ -461,7 +459,7 @@
    3.98    In principle, Isabelle tools are ordinary executable scripts that
    3.99    are run within the Isabelle settings environment, see
   3.100    \secref{sec:settings}.  The set of available tools is collected by
   3.101 -  \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} from the directories listed in the \hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOLS}}}} setting.  Do not try to call the scripts directly
   3.102 +  \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} from the directories listed in the \hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}TOOLS}}}} setting.  Do not try to call the scripts directly
   3.103    from the shell.  Neither should you add the tool directories to your
   3.104    shell's search path!%
   3.105  \end{isamarkuptext}%
   3.106 @@ -476,22 +474,22 @@
   3.107    installation like this:
   3.108  
   3.109  \begin{ttbox}
   3.110 -  isatool doc
   3.111 +  isabelle doc
   3.112  \end{ttbox}
   3.113  
   3.114    View a certain document as follows:
   3.115  \begin{ttbox}
   3.116 -  isatool doc isar-ref
   3.117 +  isabelle doc isar-ref
   3.118  \end{ttbox}
   3.119  
   3.120    Create an Isabelle session derived from HOL (see also
   3.121    \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
   3.122  \begin{ttbox}
   3.123 -  isatool mkdir HOL Test && isatool make
   3.124 +  isabelle mkdir HOL Test && isabelle make
   3.125  \end{ttbox}
   3.126 -  Note that \verb|isatool mkdir| is usually only invoked once;
   3.127 +  Note that \verb|isabelle mkdir| is usually only invoked once;
   3.128    existing sessions (including document output etc.) are then updated
   3.129 -  by \verb|isatool make| alone.%
   3.130 +  by \verb|isabelle make| alone.%
   3.131  \end{isamarkuptext}%
   3.132  \isamarkuptrue%
   3.133  %
     4.1 --- a/doc-src/System/Thy/document/Misc.tex	Sat Oct 04 17:40:56 2008 +0200
     4.2 +++ b/doc-src/System/Thy/document/Misc.tex	Sat Oct 04 17:40:58 2008 +0200
     4.3 @@ -171,7 +171,7 @@
     4.4  Get the ML system name and the location where the compiler binaries
     4.5    are supposed to reside as follows:
     4.6  \begin{ttbox}
     4.7 -isatool getenv ML_SYSTEM ML_HOME
     4.8 +isabelle getenv ML_SYSTEM ML_HOME
     4.9  {\out ML_SYSTEM=polyml}
    4.10  {\out ML_HOME=/usr/share/polyml/x86-linux}
    4.11  \end{ttbox}
    4.12 @@ -179,7 +179,7 @@
    4.13    The next one peeks at the output directory for Isabelle logic
    4.14    images:
    4.15  \begin{ttbox}
    4.16 -isatool getenv -b ISABELLE_OUTPUT
    4.17 +isabelle getenv -b ISABELLE_OUTPUT
    4.18  {\out /home/me/isabelle/heaps/polyml_x86-linux}
    4.19  \end{ttbox}
    4.20    Here we have used the \verb|-b| option to suppress the
    4.21 @@ -200,11 +200,10 @@
    4.22  \isamarkuptrue%
    4.23  %
    4.24  \begin{isamarkuptext}%
    4.25 -By default, the Isabelle binaries (\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}},
    4.26 -  \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} etc.) are just run from their location within
    4.27 -  the distribution directory, probably indirectly by the shell through
    4.28 -  its \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}.  Other schemes of installation are supported by
    4.29 -  the \indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}}} utility:
    4.30 +By default, the main Isabelle binaries (\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}
    4.31 +  etc.)  are just run from their location within the distribution
    4.32 +  directory, probably indirectly by the shell through its \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}.  Other schemes of installation are supported by the
    4.33 +  \indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}}} utility:
    4.34  \begin{ttbox}
    4.35  Usage: install [OPTIONS]
    4.36  
    4.37 @@ -221,7 +220,7 @@
    4.38    distribution directory as determined by \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}.
    4.39  
    4.40    The \verb|-p| option installs executable wrapper scripts for
    4.41 -  \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}, \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}},
    4.42 +  \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}, \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}},
    4.43    \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}, containing proper absolute references to the
    4.44    Isabelle distribution directory.  A typical \verb|DIR|
    4.45    specification would be some directory expected to be in the shell's
    4.46 @@ -249,7 +248,7 @@
    4.47      -q           quiet mode
    4.48  \end{ttbox}
    4.49    You are encouraged to use this to create a derived logo for your
    4.50 -  Isabelle project.  For example, \verb|isatool| \hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}~\verb|Bali| creates \verb|isabelle_bali.eps|.%
    4.51 +  Isabelle project.  For example, \verb|isabelle| \hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}~\verb|Bali| creates \verb|isabelle_bali.eps|.%
    4.52  \end{isamarkuptext}%
    4.53  \isamarkuptrue%
    4.54  %
    4.55 @@ -302,7 +301,7 @@
    4.56  \begin{ttbox}
    4.57  Usage: makeall [ARGS ...]
    4.58  
    4.59 -  Apply isatool make to all logics (passing ARGS).
    4.60 +  Apply isabelle make to all logics (passing ARGS).
    4.61  \end{ttbox}
    4.62  
    4.63    The arguments \verb|ARGS| are just passed verbatim to each
     5.1 --- a/doc-src/System/Thy/document/Presentation.tex	Sat Oct 04 17:40:56 2008 +0200
     5.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Sat Oct 04 17:40:58 2008 +0200
     5.3 @@ -46,22 +46,22 @@
     5.4    \begin{center}
     5.5    \begin{tabular}{lp{0.6\textwidth}}
     5.6  
     5.7 -      \verb|isatool| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} & invoked once by the user
     5.8 +      \verb|isabelle| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} & invoked once by the user
     5.9        to create the initial source setup (common \verb|IsaMakefile| plus a single session directory); \\
    5.10  
    5.11 -      \verb|isatool| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} & invoked repeatedly by the
    5.12 +      \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} & invoked repeatedly by the
    5.13        user to keep session output up-to-date (HTML, documents etc.); \\
    5.14  
    5.15 -      \verb|isatool| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} & part of the standard
    5.16 +      \verb|isabelle| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} & part of the standard
    5.17        \verb|IsaMakefile| entry of a session; \\
    5.18  
    5.19 -      \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} & run through \verb|isatool| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}; \\
    5.20 +      \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} & run through \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}; \\
    5.21  
    5.22 -      \verb|isatool| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} & run by the Isabelle
    5.23 +      \verb|isabelle| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} & run by the Isabelle
    5.24        process if document preparation is enabled; \\
    5.25  
    5.26 -      \verb|isatool| \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} & universal {\LaTeX} tool
    5.27 -      wrapper invoked multiple times by \verb|isatool| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}; also useful for manual experiments; \\
    5.28 +      \verb|isabelle| \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} & universal {\LaTeX} tool
    5.29 +      wrapper invoked multiple times by \verb|isabelle| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}; also useful for manual experiments; \\
    5.30  
    5.31    \end{tabular}
    5.32    \caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
    5.33 @@ -98,7 +98,7 @@
    5.34  
    5.35    The easiest way to let Isabelle generate theory browsing information
    5.36    for existing sessions is to append ``\verb|-i true|'' to the
    5.37 -  \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} before invoking \verb|isatool| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} (or \hyperlink{file.$ISABELLE-HOME/build}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}build}}}}).  For
    5.38 +  \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} before invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} (or \hyperlink{file.$ISABELLE-HOME/build}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}build}}}}).  For
    5.39    example, add something like this to your Isabelle settings file
    5.40  
    5.41  \begin{ttbox}
    5.42 @@ -106,7 +106,7 @@
    5.43  \end{ttbox}
    5.44  
    5.45    and then change into the \hyperlink{file.~~/src/FOL}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL}}}} directory and run
    5.46 -  \verb|isatool| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isatool| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|.  The presentation output will appear in
    5.47 +  \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|.  The presentation output will appear in
    5.48    \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
    5.49    \verb|~/isabelle/browser_info/FOL|.  Note that option
    5.50    \verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
    5.51 @@ -142,18 +142,18 @@
    5.52    copy the corresponding subdirectory from \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} to your WWW server, having generated browser
    5.53    info like this:
    5.54  \begin{ttbox}
    5.55 -isatool usedir -i true HOL Foo
    5.56 +isabelle usedir -i true HOL Foo
    5.57  \end{ttbox}
    5.58  
    5.59    This assumes that directory \verb|Foo| contains some \verb|ROOT.ML| file to load all your theories, and HOL is your parent
    5.60 -  logic image (\verb|isatool| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} assists in
    5.61 +  logic image (\verb|isabelle| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} assists in
    5.62    setting up Isabelle session directories.  Theory browser information
    5.63    for HOL should have been generated already beforehand.
    5.64    Alternatively, one may specify an external link to an existing body
    5.65    of HTML data by giving \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} a \verb|-P| option like
    5.66    this:
    5.67  \begin{ttbox}
    5.68 -isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
    5.69 +isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
    5.70  \end{ttbox}
    5.71  
    5.72    \medskip For production use, the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} tool is usually
    5.73 @@ -162,7 +162,7 @@
    5.74    provide easy setup of all this, with only minimal manual editing
    5.75    required.
    5.76  \begin{ttbox}
    5.77 -isatool mkdir HOL Foo && isatool make
    5.78 +isabelle mkdir HOL Foo && isabelle make
    5.79  \end{ttbox}
    5.80    See \secref{sec:tool-mkdir} for more information on preparing
    5.81    Isabelle session directories, including the setup for documents.%
    5.82 @@ -182,7 +182,7 @@
    5.83    hidden, thus enabling the user to collapse irrelevant portions of
    5.84    information.  The browser is written in Java, it can be used both as
    5.85    a stand-alone application and as an applet.  Note that the option
    5.86 -  \verb|-g| of \verb|isatool| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} creates
    5.87 +  \verb|-g| of \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} creates
    5.88    graph presentations in batch mode for inclusion in session
    5.89    documents.%
    5.90  \end{isamarkuptext}%
    5.91 @@ -366,7 +366,7 @@
    5.92    directory with a minimal \verb|root.tex| that is sufficient to
    5.93    print all theories of the session (in the order of appearance); see
    5.94    \secref{sec:tool-document} for further information on Isabelle
    5.95 -  document preparation.  The usage of \verb|isatool| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} is:
    5.96 +  document preparation.  The usage of \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} is:
    5.97  
    5.98  \begin{ttbox}
    5.99  Usage: mkdir [OPTIONS] [LOGIC] NAME
   5.100 @@ -431,12 +431,12 @@
   5.101    default logic, with proper document generation is generated like
   5.102    this:
   5.103  \begin{ttbox}
   5.104 -isatool mkdir Foo && isatool make
   5.105 +isabelle mkdir Foo && isabelle make
   5.106  \end{ttbox}
   5.107  
   5.108    \noindent The theory sources should be put into the \verb|Foo|
   5.109    directory, and its \verb|ROOT.ML| should be edited to load all
   5.110 -  required theories.  Invoking \verb|isatool| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} again
   5.111 +  required theories.  Invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} again
   5.112    would run the whole session, generating browser information and the
   5.113    document automatically.  The \verb|IsaMakefile| is typically
   5.114    tuned manually later, e.g.\ adding source dependencies, or changing
   5.115 @@ -447,7 +447,7 @@
   5.116    manual editing of the generated \verb|IsaMakefile|, which is
   5.117    meant to cover all of the sub-session directories at the same time
   5.118    (this is the deeper reasong why \verb|IsaMakefile| is not made
   5.119 -  part of the initial session directory created by \verb|isatool| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}).  See \hyperlink{file.~~/src/HOL/IsaMakefile}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}IsaMakefile}}}} for
   5.120 +  part of the initial session directory created by \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}).  See \hyperlink{file.~~/src/HOL/IsaMakefile}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}IsaMakefile}}}} for
   5.121    a full-blown example.%
   5.122  \end{isamarkuptext}%
   5.123  \isamarkuptrue%
   5.124 @@ -565,8 +565,8 @@
   5.125    sources to be dumped at location \verb|PATH|; this path is
   5.126    relative to the session's main directory.  If the \verb|-C|
   5.127    option is true, this will include a copy of an existing \verb|document| directory as provided by the user.  For example,
   5.128 -  \verb|isatool| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}~\verb|-D generated HOL|\isasep\isanewline%
   5.129 -\verb|  Foo| produces a complete set of document sources at \verb|Foo/generated|.  Subsequent invocation of \verb|isatool| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|Foo/generated| (see also
   5.130 +  \verb|isabelle| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}~\verb|-D generated HOL|\isasep\isanewline%
   5.131 +\verb|  Foo| produces a complete set of document sources at \verb|Foo/generated|.  Subsequent invocation of \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|Foo/generated| (see also
   5.132    \secref{sec:tool-document}) will process the final result
   5.133    independently of an Isabelle job.  This decoupled mode of operation
   5.134    facilitates debugging of serious {\LaTeX} errors, for example.
   5.135 @@ -704,7 +704,7 @@
   5.136    bookmarks), we recommend to include \hyperlink{file.~~/lib/texinputs/pdfsetup.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}pdfsetup{\isachardot}sty}}}} as well.
   5.137  
   5.138    \medskip As a final step of document preparation within Isabelle,
   5.139 -  \verb|isatool| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|-c| is run on the
   5.140 +  \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|-c| is run on the
   5.141    resulting \verb|document| directory.  Thus the actual output
   5.142    document is built and installed in its proper place (as linked by
   5.143    the session's \verb|index.html| if option \verb|-i| of
   5.144 @@ -757,7 +757,7 @@
   5.145  \isamarkuptrue%
   5.146  %
   5.147  \begin{isamarkuptext}%
   5.148 -Invoking \verb|isatool| \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} by hand may be
   5.149 +Invoking \verb|isabelle| \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} by hand may be
   5.150    occasionally useful when debugging failed attempts of the automatic
   5.151    document preparation stage of batch-mode Isabelle.  The abortive
   5.152    process leaves the sources at a certain place within \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}, see the runtime error message for details.
   5.153 @@ -765,7 +765,7 @@
   5.154    like this:
   5.155  \begin{ttbox}
   5.156    cd ~/isabelle/browser_info/HOL/Test/document
   5.157 -  isatool latex -o pdf
   5.158 +  isabelle latex -o pdf
   5.159  \end{ttbox}%
   5.160  \end{isamarkuptext}%
   5.161  \isamarkuptrue%