--- a/doc-src/System/Thy/document/Presentation.tex Mon Sep 15 20:22:38 2008 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex Mon Sep 15 20:51:40 2008 +0200
@@ -55,8 +55,7 @@
\verb|isatool usedir| & part of the standard \verb|IsaMakefile| entry of a session; \\
- \verb|isabelle-process| & run through \verb|isatool|\isasep\isanewline%
-\verb| usedir|; \\
+ \verb|isabelle-process| & run through \verb|isatool usedir|; \\
\verb|isatool document| & run by the Isabelle process if
document preparation is enabled; \\
@@ -122,7 +121,7 @@
ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
\end{ttbox}
Enabling options \verb|-i| and \verb|-d|
- simultaneausly as shown above causes an appropriate ``document''
+ simultaneously as shown above causes an appropriate ``document''
link to be included in the HTML index. Documents (or raw document
sources) may be generated independently of browser information as
well, see \secref{sec:tool-document} for further details.
@@ -131,12 +130,13 @@
sub-directory directory determined by the \indexref{}{setting}{ISABELLE\_BROWSER\_INFO}\hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}} setting plus a prefix corresponding to the
session identifier (according to the tree structure of sub-sessions
by default). A complete WWW view of all standard object-logics and
- examples of the Isabelle distribution is available at the Cambridge
- or Munich Isabelle sites:
+ examples of the Isabelle distribution is available at the usual
+ Isabelle sites:
\begin{center}\small
\begin{tabular}{l}
- \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
- \url{http://isabelle.in.tum.de/library/} \\
+ \url{http://isabelle.in.tum.de/dist/library/} \\
+ \url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/} \\
+ \url{http://mirror.cse.unsw.edu.au/pub/isabelle/dist/library/} \\
\end{tabular}
\end{center}
@@ -323,10 +323,12 @@
\begin{isamarkuptext}%
A graph definition file has the following syntax:
+ \begin{center}\small
\begin{tabular}{rcl}
\isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}\isactrlsup {\isacharplus}{\isachardoublequote}} \\
\isa{vertex} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}vertex{\isacharunderscore}name\ vertex{\isacharunderscore}ID\ dir{\isacharunderscore}name\ {\isacharbrackleft}{\isachardoublequote}}~\verb|+|~\isa{{\isachardoublequote}{\isacharbrackright}\ path\ {\isacharbrackleft}{\isachardoublequote}}~\verb|<|~\isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}~\verb|>|~\isa{{\isachardoublequote}{\isacharbrackright}\ {\isacharbraceleft}\ vertex{\isacharunderscore}ID\ {\isacharbraceright}\isactrlsup {\isacharasterisk}{\isachardoublequote}}
\end{tabular}
+ \end{center}
The meaning of the items in a vertex description is as follows:
@@ -447,9 +449,9 @@
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|\isasep\isanewline%
-\verb| mkdir|). See \verb|src/HOL/IsaMakefile| of the Isabelle
- distribution for a full-blown example.%
+ part of the initial session directory created by
+ \verb|isatool mkdir|). See \verb|src/HOL/IsaMakefile|
+ of the Isabelle distribution for a full-blown example.%
\end{isamarkuptext}%
\isamarkuptrue%
%