doc-src/System/Thy/Presentation.thy
changeset 28225 5d1fc22bccdf
parent 28221 ca9fdab0f971
child 28238 398bf960d3d4
     1.1 --- a/doc-src/System/Thy/Presentation.thy	Mon Sep 15 20:22:38 2008 +0200
     1.2 +++ b/doc-src/System/Thy/Presentation.thy	Mon Sep 15 20:51:40 2008 +0200
     1.3 @@ -38,8 +38,7 @@
     1.4        @{verbatim "isatool usedir"} & part of the standard @{verbatim
     1.5        IsaMakefile} entry of a session; \\
     1.6  
     1.7 -      @{verbatim "isabelle-process"} & run through @{verbatim "isatool
     1.8 -      usedir"}; \\
     1.9 +      @{verbatim "isabelle-process"} & run through @{verbatim "isatool usedir"}; \\
    1.10  
    1.11        @{verbatim "isatool document"} & run by the Isabelle process if
    1.12        document preparation is enabled; \\
    1.13 @@ -105,7 +104,7 @@
    1.14  ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
    1.15  \end{ttbox}
    1.16    Enabling options @{verbatim "-i"} and @{verbatim "-d"}
    1.17 -  simultaneausly as shown above causes an appropriate ``document''
    1.18 +  simultaneously as shown above causes an appropriate ``document''
    1.19    link to be included in the HTML index.  Documents (or raw document
    1.20    sources) may be generated independently of browser information as
    1.21    well, see \secref{sec:tool-document} for further details.
    1.22 @@ -115,12 +114,13 @@
    1.23    ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the
    1.24    session identifier (according to the tree structure of sub-sessions
    1.25    by default).  A complete WWW view of all standard object-logics and
    1.26 -  examples of the Isabelle distribution is available at the Cambridge
    1.27 -  or Munich Isabelle sites:
    1.28 +  examples of the Isabelle distribution is available at the usual
    1.29 +  Isabelle sites:
    1.30    \begin{center}\small
    1.31    \begin{tabular}{l}
    1.32 -    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
    1.33 -    \url{http://isabelle.in.tum.de/library/} \\
    1.34 +    \url{http://isabelle.in.tum.de/dist/library/} \\
    1.35 +    \url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/} \\
    1.36 +    \url{http://mirror.cse.unsw.edu.au/pub/isabelle/dist/library/} \\
    1.37    \end{tabular}
    1.38    \end{center}
    1.39    
    1.40 @@ -296,10 +296,12 @@
    1.41  text {*
    1.42    A graph definition file has the following syntax:
    1.43  
    1.44 +  \begin{center}\small
    1.45    \begin{tabular}{rcl}
    1.46      @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}\<^sup>+"} \\
    1.47      @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }\<^sup>*"}
    1.48    \end{tabular}
    1.49 +  \end{center}
    1.50  
    1.51    The meaning of the items in a vertex description is as follows:
    1.52  
    1.53 @@ -418,9 +420,9 @@
    1.54    manual editing of the generated @{verbatim IsaMakefile}, which is
    1.55    meant to cover all of the sub-session directories at the same time
    1.56    (this is the deeper reasong why @{verbatim IsaMakefile} is not made
    1.57 -  part of the initial session directory created by @{verbatim "isatool
    1.58 -  mkdir"}).  See @{verbatim "src/HOL/IsaMakefile"} of the Isabelle
    1.59 -  distribution for a full-blown example.
    1.60 +  part of the initial session directory created by
    1.61 +  @{verbatim "isatool mkdir"}).  See @{verbatim "src/HOL/IsaMakefile"}
    1.62 +  of the Isabelle distribution for a full-blown example.
    1.63  *}
    1.64  
    1.65