# HG changeset patch
# User wenzelm
# Date 1221504700 -7200
# Node ID 5d1fc22bccdf6925372ddbdf610ae64be98a1df2
# Parent  10487d954a8fa89ceaf10fe617be6f9576e6258f
tuned;

diff -r 10487d954a8f -r 5d1fc22bccdf doc-src/System/Thy/Presentation.thy
--- a/doc-src/System/Thy/Presentation.thy	Mon Sep 15 20:22:38 2008 +0200
+++ b/doc-src/System/Thy/Presentation.thy	Mon Sep 15 20:51:40 2008 +0200
@@ -38,8 +38,7 @@
       @{verbatim "isatool usedir"} & part of the standard @{verbatim
       IsaMakefile} entry of a session; \\
 
-      @{verbatim "isabelle-process"} & run through @{verbatim "isatool
-      usedir"}; \\
+      @{verbatim "isabelle-process"} & run through @{verbatim "isatool usedir"}; \\
 
       @{verbatim "isatool document"} & run by the Isabelle process if
       document preparation is enabled; \\
@@ -105,7 +104,7 @@
 ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
 \end{ttbox}
   Enabling options @{verbatim "-i"} and @{verbatim "-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.
@@ -115,12 +114,13 @@
   ISABELLE_BROWSER_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}
   
@@ -296,10 +296,12 @@
 text {*
   A graph definition file has the following syntax:
 
+  \begin{center}\small
   \begin{tabular}{rcl}
     @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\
     @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"}
   \end{tabular}
+  \end{center}
 
   The meaning of the items in a vertex description is as follows:
 
@@ -418,9 +420,9 @@
   manual editing of the generated @{verbatim IsaMakefile}, which is
   meant to cover all of the sub-session directories at the same time
   (this is the deeper reasong why @{verbatim IsaMakefile} is not made
-  part of the initial session directory created by @{verbatim "isatool
-  mkdir"}).  See @{verbatim "src/HOL/IsaMakefile"} of the Isabelle
-  distribution for a full-blown example.
+  part of the initial session directory created by
+  @{verbatim "isatool mkdir"}).  See @{verbatim "src/HOL/IsaMakefile"}
+  of the Isabelle distribution for a full-blown example.
 *}
 
 
diff -r 10487d954a8f -r 5d1fc22bccdf doc-src/System/Thy/document/Presentation.tex
--- 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%
 %