1.1 --- a/doc-src/System/Thy/Misc.thy	Sat Oct 04 16:19:49 2008 +0200
     1.2 +++ b/doc-src/System/Thy/Misc.thy	Sat Oct 04 17:40:56 2008 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4    Get the ML system name and the location where the compiler binaries
     1.5    are supposed to reside as follows:
     1.6  \begin{ttbox}
     1.7 -isatool getenv ML_SYSTEM ML_HOME
     1.8 +isabelle getenv ML_SYSTEM ML_HOME
     1.9  {\out ML_SYSTEM=polyml}
    1.10  {\out ML_HOME=/usr/share/polyml/x86-linux}
    1.11  \end{ttbox}
    1.12 @@ -152,7 +152,7 @@
    1.13    The next one peeks at the output directory for Isabelle logic
    1.14    images:
    1.15  \begin{ttbox}
    1.16 -isatool getenv -b ISABELLE_OUTPUT
    1.17 +isabelle getenv -b ISABELLE_OUTPUT
    1.18  {\out /home/me/isabelle/heaps/polyml_x86-linux}
    1.19  \end{ttbox}
    1.20    Here we have used the @{verbatim "-b"} option to suppress the
    1.21 @@ -171,11 +171,11 @@
    1.22  section {* Installing standalone Isabelle executables \label{sec:tool-install} *}
    1.23  
    1.24  text {*
    1.25 -  By default, the Isabelle binaries (@{executable "isabelle-process"},
    1.26 -  @{executable isatool} etc.) are just run from their location within
    1.27 -  the distribution directory, probably indirectly by the shell through
    1.28 -  its @{setting PATH}.  Other schemes of installation are supported by
    1.29 -  the @{tool_def install} utility:
    1.30 +  By default, the main Isabelle binaries (@{executable "isabelle"}
    1.31 +  etc.)  are just run from their location within the distribution
    1.32 +  directory, probably indirectly by the shell through its @{setting
    1.33 +  PATH}.  Other schemes of installation are supported by the
    1.34 +  @{tool_def install} utility:
    1.35  \begin{ttbox}
    1.36  Usage: install [OPTIONS]
    1.37  
    1.38 @@ -192,7 +192,7 @@
    1.39    distribution directory as determined by @{setting ISABELLE_HOME}.
    1.40  
    1.41    The @{verbatim "-p"} option installs executable wrapper scripts for
    1.42 -  @{executable "isabelle-process"}, @{executable isatool},
    1.43 +  @{executable "isabelle-process"}, @{executable isabelle},
    1.44    @{executable Isabelle}, containing proper absolute references to the
    1.45    Isabelle distribution directory.  A typical @{verbatim DIR}
    1.46    specification would be some directory expected to be in the shell's
    1.47 @@ -218,7 +218,7 @@
    1.48      -q           quiet mode
    1.49  \end{ttbox}
    1.50    You are encouraged to use this to create a derived logo for your
    1.51 -  Isabelle project.  For example, @{verbatim isatool} @{tool
    1.52 +  Isabelle project.  For example, @{verbatim isabelle} @{tool
    1.53    logo}~@{verbatim Bali} creates @{verbatim isabelle_bali.eps}.
    1.54  *}
    1.55  
    1.56 @@ -267,7 +267,7 @@
    1.57  \begin{ttbox}
    1.58  Usage: makeall [ARGS ...]
    1.59  
    1.60 -  Apply isatool make to all logics (passing ARGS).
    1.61 +  Apply isabelle make to all logics (passing ARGS).
    1.62  \end{ttbox}
    1.63  
    1.64    The arguments @{verbatim ARGS} are just passed verbatim to each