--- a/doc-src/TutorialI/Documents/document/Documents.tex Tue Nov 18 18:22:49 2008 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Tue Nov 18 18:25:10 2008 +0100
@@ -123,7 +123,7 @@
\verb,\,\verb,<forall>, symbol as~\isa{{\isasymforall}}.
A list of standard Isabelle symbols is given in
- \cite[appendix~A]{isabelle-sys}. You may introduce your own
+ \cite{isabelle-isar-ref}. You may introduce your own
interpretation of further symbols by configuring the appropriate
front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
@@ -394,18 +394,18 @@
(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
@@ -441,7 +441,7 @@
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}
@@ -464,7 +464,7 @@
\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
@@ -741,7 +741,7 @@
straightforward generalization of ASCII characters. While Isabelle
does not impose any interpretation of the infinite collection of
named symbols, {\LaTeX} documents use canonical glyphs for certain
- standard symbols \cite[appendix~A]{isabelle-sys}.
+ standard symbols \cite{isabelle-isar-ref}.
The {\LaTeX} code produced from Isabelle text follows a simple
scheme. You can tune the final appearance by redefining certain
@@ -844,7 +844,7 @@
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