--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Sat Oct 04 17:40:56 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Sat Oct 04 17:40:58 2008 +0200
@@ -36,10 +36,10 @@
easy by using the Isabelle \verb|mkdir| and \verb|make|
tools. First invoke
\begin{ttbox}
- isatool mkdir Foo
+ isabelle mkdir Foo
\end{ttbox}
to initialize a separate directory for session \verb|Foo| ---
- it is safe to experiment, since \verb|isatool mkdir| never
+ it is safe to experiment, since \verb|isabelle mkdir| never
overwrites existing files. Ensure that \verb|Foo/ROOT.ML|
holds ML commands to load all theories required for this session;
furthermore \verb|Foo/document/root.tex| should include any
@@ -51,7 +51,7 @@
one level up from the \verb|Foo| directory location. Now
invoke
\begin{ttbox}
- isatool make Foo
+ isabelle make Foo
\end{ttbox}
to run the \verb|Foo| session, with browser information and
document preparation enabled. Unless any errors are reported by
--- a/doc-src/IsarRef/Thy/document/Introduction.tex Sat Oct 04 17:40:56 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Introduction.tex Sat Oct 04 17:40:58 2008 +0200
@@ -105,7 +105,7 @@
the Isar interaction loop, with some support for command line
editing. For example:
\begin{ttbox}
-isatool tty\medskip
+isabelle tty\medskip
{\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip
theory Foo imports Main begin;
definition foo :: nat where "foo == 1";
--- a/doc-src/System/Thy/document/Basics.tex Sat Oct 04 17:40:56 2008 +0200
+++ b/doc-src/System/Thy/document/Basics.tex Sat Oct 04 17:40:58 2008 +0200
@@ -40,21 +40,19 @@
variables to all Isabelle programs (including tools and user
interfaces).
- \item The \emph{raw Isabelle process} (\indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} or
- \indexref{}{executable}{isabelle-process}\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}) runs logic sessions either
- interactively or in batch mode. In particular, this view abstracts
- over the invocation of the actual ML system to be used. Regular
- users rarely need to care about the low-level process.
+ \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
+ batch mode. In particular, this view abstracts over the invocation
+ of the actual ML system to be used. Regular users rarely need to
+ care about the low-level process.
- \item The \emph{Isabelle tools wrapper} (\indexref{}{executable}{isatool}\hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}})
+ \item The \emph{Isabelle tools wrapper} (\indexref{}{executable}{isabelle}\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}})
provides a generic startup environment Isabelle related utilities,
user interfaces etc. Such tools automatically benefit from the
settings mechanism.
- \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
- abstraction over the actual user interface to be used. The de-facto
- standard interface for Isabelle is Proof~General
- \cite{proofgeneral}.
+ \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
+ user interface to be used. The de-facto standard interface for
+ Isabelle is Proof~General \cite{proofgeneral}.
\end{enumerate}%
\end{isamarkuptext}%
@@ -144,7 +142,7 @@
\begin{itemize}
\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
- 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,
+ 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,
respectively.
\item \indexref{}{setting}{ISABELLE\_OUTPUT}\hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}} will have the identifiers of
@@ -186,7 +184,7 @@
a private \verb|$ISABELLE_HOME_USER/etc/settings|.
\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
- 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
+ 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
need not assume that the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}bin}}}} directory is
on the current search path of the shell.
@@ -241,8 +239,8 @@
document preparation (see also \secref{sec:tool-latex}).
\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
- directories that are scanned by \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} for external
- utility programs (see also \secref{sec:isatool}).
+ directories that are scanned by \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} for external
+ utility programs (see also \secref{sec:isabelle-tool}).
\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
directories with documentation files.
@@ -277,10 +275,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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
- sessions --- either interactively or in batch mode. It provides an
- abstraction over the underlying ML system, and over the actual heap
- file locations. Its usage is:
+The \indexdef{}{executable}{isabelle-process}\hypertarget{executable.isabelle-process}{\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}} executable runs bare-bones
+ Isabelle logic sessions --- either interactively or in batch mode.
+ It provides an abstraction over the underlying ML system, and over
+ the actual heap file locations. Its usage is:
\begin{ttbox}
Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
@@ -438,16 +436,16 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{The Isabelle tools wrapper \label{sec:isatool}%
+\isamarkupsection{The Isabelle tools wrapper \label{sec:isabelle-tool}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
All Isabelle related tools and interfaces are called via a common
- wrapper --- \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}}:
+ wrapper --- \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}:
\begin{ttbox}
-Usage: isatool TOOL [ARGS ...]
+Usage: isabelle TOOL [ARGS ...]
Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
for more specific help.
@@ -461,7 +459,7 @@
In principle, Isabelle tools are ordinary executable scripts that
are run within the Isabelle settings environment, see
\secref{sec:settings}. The set of available tools is collected by
- \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
+ \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
from the shell. Neither should you add the tool directories to your
shell's search path!%
\end{isamarkuptext}%
@@ -476,22 +474,22 @@
installation like this:
\begin{ttbox}
- isatool doc
+ isabelle doc
\end{ttbox}
View a certain document as follows:
\begin{ttbox}
- isatool doc isar-ref
+ isabelle doc isar-ref
\end{ttbox}
Create an Isabelle session derived from HOL (see also
\secref{sec:tool-mkdir} and \secref{sec:tool-make}):
\begin{ttbox}
- isatool mkdir HOL Test && isatool make
+ isabelle mkdir HOL Test && isabelle make
\end{ttbox}
- Note that \verb|isatool mkdir| is usually only invoked once;
+ Note that \verb|isabelle mkdir| is usually only invoked once;
existing sessions (including document output etc.) are then updated
- by \verb|isatool make| alone.%
+ by \verb|isabelle make| alone.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/System/Thy/document/Misc.tex Sat Oct 04 17:40:56 2008 +0200
+++ b/doc-src/System/Thy/document/Misc.tex Sat Oct 04 17:40:58 2008 +0200
@@ -171,7 +171,7 @@
Get the ML system name and the location where the compiler binaries
are supposed to reside as follows:
\begin{ttbox}
-isatool getenv ML_SYSTEM ML_HOME
+isabelle getenv ML_SYSTEM ML_HOME
{\out ML_SYSTEM=polyml}
{\out ML_HOME=/usr/share/polyml/x86-linux}
\end{ttbox}
@@ -179,7 +179,7 @@
The next one peeks at the output directory for Isabelle logic
images:
\begin{ttbox}
-isatool getenv -b ISABELLE_OUTPUT
+isabelle getenv -b ISABELLE_OUTPUT
{\out /home/me/isabelle/heaps/polyml_x86-linux}
\end{ttbox}
Here we have used the \verb|-b| option to suppress the
@@ -200,11 +200,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-By default, the Isabelle binaries (\hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}},
- \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} etc.) are just run from their location within
- the distribution directory, probably indirectly by the shell through
- its \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}. Other schemes of installation are supported by
- the \indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}}} utility:
+By default, the main Isabelle binaries (\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}
+ etc.) are just run from their location within the distribution
+ directory, probably indirectly by the shell through its \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}. Other schemes of installation are supported by the
+ \indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}}} utility:
\begin{ttbox}
Usage: install [OPTIONS]
@@ -221,7 +220,7 @@
distribution directory as determined by \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}.
The \verb|-p| option installs executable wrapper scripts for
- \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}, \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}},
+ \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}}, \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}},
\hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}, containing proper absolute references to the
Isabelle distribution directory. A typical \verb|DIR|
specification would be some directory expected to be in the shell's
@@ -249,7 +248,7 @@
-q quiet mode
\end{ttbox}
You are encouraged to use this to create a derived logo for your
- Isabelle project. For example, \verb|isatool| \hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}~\verb|Bali| creates \verb|isabelle_bali.eps|.%
+ Isabelle project. For example, \verb|isabelle| \hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}~\verb|Bali| creates \verb|isabelle_bali.eps|.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -302,7 +301,7 @@
\begin{ttbox}
Usage: makeall [ARGS ...]
- Apply isatool make to all logics (passing ARGS).
+ Apply isabelle make to all logics (passing ARGS).
\end{ttbox}
The arguments \verb|ARGS| are just passed verbatim to each
--- a/doc-src/System/Thy/document/Presentation.tex Sat Oct 04 17:40:56 2008 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex Sat Oct 04 17:40:58 2008 +0200
@@ -46,22 +46,22 @@
\begin{center}
\begin{tabular}{lp{0.6\textwidth}}
- \verb|isatool| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} & invoked once by the user
+ \verb|isabelle| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} & invoked once by the user
to create the initial source setup (common \verb|IsaMakefile| plus a single session directory); \\
- \verb|isatool| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} & invoked repeatedly by the
+ \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} & invoked repeatedly by the
user to keep session output up-to-date (HTML, documents etc.); \\
- \verb|isatool| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} & part of the standard
+ \verb|isabelle| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} & part of the standard
\verb|IsaMakefile| entry of a session; \\
- \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} & run through \verb|isatool| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}; \\
+ \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isacharminus}process}}}} & run through \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}; \\
- \verb|isatool| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} & run by the Isabelle
+ \verb|isabelle| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}} & run by the Isabelle
process if document preparation is enabled; \\
- \verb|isatool| \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} & universal {\LaTeX} tool
- wrapper invoked multiple times by \verb|isatool| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}; also useful for manual experiments; \\
+ \verb|isabelle| \indexref{}{tool}{latex}\hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} & universal {\LaTeX} tool
+ wrapper invoked multiple times by \verb|isabelle| \indexref{}{tool}{document}\hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}; also useful for manual experiments; \\
\end{tabular}
\caption{The tool chain of Isabelle session presentation} \label{fig:session-tools}
@@ -98,7 +98,7 @@
The easiest way to let Isabelle generate theory browsing information
for existing sessions is to append ``\verb|-i true|'' to the
- \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
+ \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
example, add something like this to your Isabelle settings file
\begin{ttbox}
@@ -106,7 +106,7 @@
\end{ttbox}
and then change into the \hyperlink{file.~~/src/FOL}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL}}}} directory and run
- \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
+ \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
\verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
\verb|~/isabelle/browser_info/FOL|. Note that option
\verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
@@ -142,18 +142,18 @@
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
info like this:
\begin{ttbox}
-isatool usedir -i true HOL Foo
+isabelle usedir -i true HOL Foo
\end{ttbox}
This assumes that directory \verb|Foo| contains some \verb|ROOT.ML| file to load all your theories, and HOL is your parent
- logic image (\verb|isatool| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} assists in
+ logic image (\verb|isabelle| \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} assists in
setting up Isabelle session directories. Theory browser information
for HOL should have been generated already beforehand.
Alternatively, one may specify an external link to an existing body
of HTML data by giving \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} a \verb|-P| option like
this:
\begin{ttbox}
-isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
+isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
\end{ttbox}
\medskip For production use, the \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} tool is usually
@@ -162,7 +162,7 @@
provide easy setup of all this, with only minimal manual editing
required.
\begin{ttbox}
-isatool mkdir HOL Foo && isatool make
+isabelle mkdir HOL Foo && isabelle make
\end{ttbox}
See \secref{sec:tool-mkdir} for more information on preparing
Isabelle session directories, including the setup for documents.%
@@ -182,7 +182,7 @@
hidden, thus enabling the user to collapse irrelevant portions of
information. The browser is written in Java, it can be used both as
a stand-alone application and as an applet. Note that the option
- \verb|-g| of \verb|isatool| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} creates
+ \verb|-g| of \verb|isabelle| \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} creates
graph presentations in batch mode for inclusion in session
documents.%
\end{isamarkuptext}%
@@ -366,7 +366,7 @@
directory with a minimal \verb|root.tex| that is sufficient to
print all theories of the session (in the order of appearance); see
\secref{sec:tool-document} for further information on Isabelle
- document preparation. The usage of \verb|isatool| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} is:
+ document preparation. The usage of \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} is:
\begin{ttbox}
Usage: mkdir [OPTIONS] [LOGIC] NAME
@@ -431,12 +431,12 @@
default logic, with proper document generation is generated like
this:
\begin{ttbox}
-isatool mkdir Foo && isatool make
+isabelle mkdir Foo && isabelle make
\end{ttbox}
\noindent The theory sources should be put into the \verb|Foo|
directory, and its \verb|ROOT.ML| should be edited to load all
- required theories. Invoking \verb|isatool| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} again
+ required theories. Invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} again
would run the whole session, generating browser information and the
document automatically. The \verb|IsaMakefile| is typically
tuned manually later, e.g.\ adding source dependencies, or changing
@@ -447,7 +447,7 @@
manual editing of the generated \verb|IsaMakefile|, which is
meant to cover all of the sub-session directories at the same time
(this is the deeper reasong why \verb|IsaMakefile| is not made
- 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
+ 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
a full-blown example.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -565,8 +565,8 @@
sources to be dumped at location \verb|PATH|; this path is
relative to the session's main directory. If the \verb|-C|
option is true, this will include a copy of an existing \verb|document| directory as provided by the user. For example,
- \verb|isatool| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}~\verb|-D generated HOL|\isasep\isanewline%
-\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
+ \verb|isabelle| \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}~\verb|-D generated HOL|\isasep\isanewline%
+\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
\secref{sec:tool-document}) will process the final result
independently of an Isabelle job. This decoupled mode of operation
facilitates debugging of serious {\LaTeX} errors, for example.
@@ -704,7 +704,7 @@
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.
\medskip As a final step of document preparation within Isabelle,
- \verb|isatool| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|-c| is run on the
+ \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|-c| is run on the
resulting \verb|document| directory. Thus the actual output
document is built and installed in its proper place (as linked by
the session's \verb|index.html| if option \verb|-i| of
@@ -757,7 +757,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Invoking \verb|isatool| \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} by hand may be
+Invoking \verb|isabelle| \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} by hand may be
occasionally useful when debugging failed attempts of the automatic
document preparation stage of batch-mode Isabelle. The abortive
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.
@@ -765,7 +765,7 @@
like this:
\begin{ttbox}
cd ~/isabelle/browser_info/HOL/Test/document
- isatool latex -o pdf
+ isabelle latex -o pdf
\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%