doc-src/System/Thy/document/Misc.tex
changeset 28505 f98751bd715f
parent 28253 04fc1ba19f93
child 28916 0a802cdda340
     1.1 --- a/doc-src/System/Thy/document/Misc.tex	Sat Oct 04 17:40:56 2008 +0200
     1.2 +++ b/doc-src/System/Thy/document/Misc.tex	Sat Oct 04 17:40:58 2008 +0200
     1.3 @@ -171,7 +171,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 @@ -179,7 +179,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 \verb|-b| option to suppress the
    1.21 @@ -200,11 +200,10 @@
    1.22  \isamarkuptrue%
    1.23  %
    1.24  \begin{isamarkuptext}%
    1.25 -By default, the Isabelle binaries (\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}},
    1.26 -  \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} etc.) are just run from their location within
    1.27 -  the distribution directory, probably indirectly by the shell through
    1.28 -  its \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}.  Other schemes of installation are supported by
    1.29 -  the \indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}}} utility:
    1.30 +By default, the main Isabelle binaries (\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}
    1.31 +  etc.)  are just run from their location within the distribution
    1.32 +  directory, probably indirectly by the shell through its \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}.  Other schemes of installation are supported by the
    1.33 +  \indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}}} utility:
    1.34  \begin{ttbox}
    1.35  Usage: install [OPTIONS]
    1.36  
    1.37 @@ -221,7 +220,7 @@
    1.38    distribution directory as determined by \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}.
    1.39  
    1.40    The \verb|-p| option installs executable wrapper scripts for
    1.41 -  \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}, \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}},
    1.42 +  \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}, \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}},
    1.43    \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}, containing proper absolute references to the
    1.44    Isabelle distribution directory.  A typical \verb|DIR|
    1.45    specification would be some directory expected to be in the shell's
    1.46 @@ -249,7 +248,7 @@
    1.47      -q           quiet mode
    1.48  \end{ttbox}
    1.49    You are encouraged to use this to create a derived logo for your
    1.50 -  Isabelle project.  For example, \verb|isatool| \hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}~\verb|Bali| creates \verb|isabelle_bali.eps|.%
    1.51 +  Isabelle project.  For example, \verb|isabelle| \hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}~\verb|Bali| creates \verb|isabelle_bali.eps|.%
    1.52  \end{isamarkuptext}%
    1.53  \isamarkuptrue%
    1.54  %
    1.55 @@ -302,7 +301,7 @@
    1.56  \begin{ttbox}
    1.57  Usage: makeall [ARGS ...]
    1.58  
    1.59 -  Apply isatool make to all logics (passing ARGS).
    1.60 +  Apply isabelle make to all logics (passing ARGS).
    1.61  \end{ttbox}
    1.62  
    1.63    The arguments \verb|ARGS| are just passed verbatim to each