tuned;
authorwenzelm
Mon Sep 15 20:51:40 2008 +0200 (2008-09-15 ago)
changeset 282255d1fc22bccdf
parent 28224 10487d954a8f
child 28226 97c530dc8aca
tuned;
doc-src/System/Thy/Presentation.thy
doc-src/System/Thy/document/Presentation.tex
     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  
     2.1 --- a/doc-src/System/Thy/document/Presentation.tex	Mon Sep 15 20:22:38 2008 +0200
     2.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Mon Sep 15 20:51:40 2008 +0200
     2.3 @@ -55,8 +55,7 @@
     2.4  
     2.5        \verb|isatool usedir| & part of the standard \verb|IsaMakefile| entry of a session; \\
     2.6  
     2.7 -      \verb|isabelle-process| & run through \verb|isatool|\isasep\isanewline%
     2.8 -\verb|      usedir|; \\
     2.9 +      \verb|isabelle-process| & run through \verb|isatool usedir|; \\
    2.10  
    2.11        \verb|isatool document| & run by the Isabelle process if
    2.12        document preparation is enabled; \\
    2.13 @@ -122,7 +121,7 @@
    2.14  ISABELLE_USEDIR_OPTIONS="-i true -d dvi"
    2.15  \end{ttbox}
    2.16    Enabling options \verb|-i| and \verb|-d|
    2.17 -  simultaneausly as shown above causes an appropriate ``document''
    2.18 +  simultaneously as shown above causes an appropriate ``document''
    2.19    link to be included in the HTML index.  Documents (or raw document
    2.20    sources) may be generated independently of browser information as
    2.21    well, see \secref{sec:tool-document} for further details.
    2.22 @@ -131,12 +130,13 @@
    2.23    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
    2.24    session identifier (according to the tree structure of sub-sessions
    2.25    by default).  A complete WWW view of all standard object-logics and
    2.26 -  examples of the Isabelle distribution is available at the Cambridge
    2.27 -  or Munich Isabelle sites:
    2.28 +  examples of the Isabelle distribution is available at the usual
    2.29 +  Isabelle sites:
    2.30    \begin{center}\small
    2.31    \begin{tabular}{l}
    2.32 -    \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
    2.33 -    \url{http://isabelle.in.tum.de/library/} \\
    2.34 +    \url{http://isabelle.in.tum.de/dist/library/} \\
    2.35 +    \url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/} \\
    2.36 +    \url{http://mirror.cse.unsw.edu.au/pub/isabelle/dist/library/} \\
    2.37    \end{tabular}
    2.38    \end{center}
    2.39    
    2.40 @@ -323,10 +323,12 @@
    2.41  \begin{isamarkuptext}%
    2.42  A graph definition file has the following syntax:
    2.43  
    2.44 +  \begin{center}\small
    2.45    \begin{tabular}{rcl}
    2.46      \isa{graph} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharbraceleft}\ vertex{\isachardoublequote}}~\verb|;|~\isa{{\isachardoublequote}{\isacharbraceright}\isactrlsup {\isacharplus}{\isachardoublequote}} \\
    2.47      \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}}
    2.48    \end{tabular}
    2.49 +  \end{center}
    2.50  
    2.51    The meaning of the items in a vertex description is as follows:
    2.52  
    2.53 @@ -447,9 +449,9 @@
    2.54    manual editing of the generated \verb|IsaMakefile|, which is
    2.55    meant to cover all of the sub-session directories at the same time
    2.56    (this is the deeper reasong why \verb|IsaMakefile| is not made
    2.57 -  part of the initial session directory created by \verb|isatool|\isasep\isanewline%
    2.58 -\verb|  mkdir|).  See \verb|src/HOL/IsaMakefile| of the Isabelle
    2.59 -  distribution for a full-blown example.%
    2.60 +  part of the initial session directory created by
    2.61 +  \verb|isatool mkdir|).  See \verb|src/HOL/IsaMakefile|
    2.62 +  of the Isabelle distribution for a full-blown example.%
    2.63  \end{isamarkuptext}%
    2.64  \isamarkuptrue%
    2.65  %