doc-src/System/Thy/Presentation.thy
changeset 28504 7ad7d7d6df47
parent 28238 398bf960d3d4
child 28838 d5db6dfcb34a
     1.1 --- a/doc-src/System/Thy/Presentation.thy	Sat Oct 04 16:19:49 2008 +0200
     1.2 +++ b/doc-src/System/Thy/Presentation.thy	Sat Oct 04 17:40:56 2008 +0200
     1.3 @@ -28,24 +28,24 @@
     1.4    \begin{center}
     1.5    \begin{tabular}{lp{0.6\textwidth}}
     1.6  
     1.7 -      @{verbatim isatool} @{tool_ref mkdir} & invoked once by the user
     1.8 +      @{verbatim isabelle} @{tool_ref mkdir} & invoked once by the user
     1.9        to create the initial source setup (common @{verbatim
    1.10        IsaMakefile} plus a single session directory); \\
    1.11  
    1.12 -      @{verbatim isatool} @{tool make} & invoked repeatedly by the
    1.13 +      @{verbatim isabelle} @{tool make} & invoked repeatedly by the
    1.14        user to keep session output up-to-date (HTML, documents etc.); \\
    1.15  
    1.16 -      @{verbatim isatool} @{tool usedir} & part of the standard
    1.17 +      @{verbatim isabelle} @{tool usedir} & part of the standard
    1.18        @{verbatim IsaMakefile} entry of a session; \\
    1.19  
    1.20        @{executable "isabelle-process"} & run through @{verbatim
    1.21 -      isatool} @{tool_ref usedir}; \\
    1.22 +      isabelle} @{tool_ref usedir}; \\
    1.23  
    1.24 -      @{verbatim isatool} @{tool_ref document} & run by the Isabelle
    1.25 +      @{verbatim isabelle} @{tool_ref document} & run by the Isabelle
    1.26        process if document preparation is enabled; \\
    1.27  
    1.28 -      @{verbatim isatool} @{tool_ref latex} & universal {\LaTeX} tool
    1.29 -      wrapper invoked multiple times by @{verbatim isatool} @{tool_ref
    1.30 +      @{verbatim isabelle} @{tool_ref latex} & universal {\LaTeX} tool
    1.31 +      wrapper invoked multiple times by @{verbatim isabelle} @{tool_ref
    1.32        document}; also useful for manual experiments; \\
    1.33  
    1.34    \end{tabular}
    1.35 @@ -82,7 +82,7 @@
    1.36    The easiest way to let Isabelle generate theory browsing information
    1.37    for existing sessions is to append ``@{verbatim "-i true"}'' to the
    1.38    @{setting_ref ISABELLE_USEDIR_OPTIONS} before invoking @{verbatim
    1.39 -  isatool} @{tool make} (or @{"file" "$ISABELLE_HOME/build"}).  For
    1.40 +  isabelle} @{tool make} (or @{"file" "$ISABELLE_HOME/build"}).  For
    1.41    example, add something like this to your Isabelle settings file
    1.42  
    1.43  \begin{ttbox}
    1.44 @@ -90,7 +90,7 @@
    1.45  \end{ttbox}
    1.46  
    1.47    and then change into the @{"file" "~~/src/FOL"} directory and run
    1.48 -  @{verbatim isatool} @{tool make}, or even @{verbatim isatool} @{tool
    1.49 +  @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle} @{tool
    1.50    make}~@{verbatim all}.  The presentation output will appear in
    1.51    @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
    1.52    @{verbatim "~/isabelle/browser_info/FOL"}.  Note that option
    1.53 @@ -130,19 +130,19 @@
    1.54    ISABELLE_BROWSER_INFO} to your WWW server, having generated browser
    1.55    info like this:
    1.56  \begin{ttbox}
    1.57 -isatool usedir -i true HOL Foo
    1.58 +isabelle usedir -i true HOL Foo
    1.59  \end{ttbox}
    1.60  
    1.61    This assumes that directory @{verbatim Foo} contains some @{verbatim
    1.62    ROOT.ML} file to load all your theories, and HOL is your parent
    1.63 -  logic image (@{verbatim isatool} @{tool_ref mkdir} assists in
    1.64 +  logic image (@{verbatim isabelle} @{tool_ref mkdir} assists in
    1.65    setting up Isabelle session directories.  Theory browser information
    1.66    for HOL should have been generated already beforehand.
    1.67    Alternatively, one may specify an external link to an existing body
    1.68    of HTML data by giving @{tool usedir} a @{verbatim "-P"} option like
    1.69    this:
    1.70  \begin{ttbox}
    1.71 -isatool usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
    1.72 +isabelle usedir -i true -P http://isabelle.in.tum.de/library/ HOL Foo
    1.73  \end{ttbox}
    1.74  
    1.75    \medskip For production use, the @{tool usedir} tool is usually
    1.76 @@ -151,7 +151,7 @@
    1.77    provide easy setup of all this, with only minimal manual editing
    1.78    required.
    1.79  \begin{ttbox}
    1.80 -isatool mkdir HOL Foo && isatool make
    1.81 +isabelle mkdir HOL Foo && isabelle make
    1.82  \end{ttbox}
    1.83    See \secref{sec:tool-mkdir} for more information on preparing
    1.84    Isabelle session directories, including the setup for documents.
    1.85 @@ -169,7 +169,7 @@
    1.86    hidden, thus enabling the user to collapse irrelevant portions of
    1.87    information.  The browser is written in Java, it can be used both as
    1.88    a stand-alone application and as an applet.  Note that the option
    1.89 -  @{verbatim "-g"} of @{verbatim isatool} @{tool_ref usedir} creates
    1.90 +  @{verbatim "-g"} of @{verbatim isabelle} @{tool_ref usedir} creates
    1.91    graph presentations in batch mode for inclusion in session
    1.92    documents.
    1.93  *}
    1.94 @@ -342,7 +342,7 @@
    1.95    directory with a minimal @{verbatim root.tex} that is sufficient to
    1.96    print all theories of the session (in the order of appearance); see
    1.97    \secref{sec:tool-document} for further information on Isabelle
    1.98 -  document preparation.  The usage of @{verbatim isatool} @{tool
    1.99 +  document preparation.  The usage of @{verbatim isabelle} @{tool
   1.100    mkdir} is:
   1.101  
   1.102  \begin{ttbox}
   1.103 @@ -406,12 +406,12 @@
   1.104    default logic, with proper document generation is generated like
   1.105    this:
   1.106  \begin{ttbox}
   1.107 -isatool mkdir Foo && isatool make
   1.108 +isabelle mkdir Foo && isabelle make
   1.109  \end{ttbox}
   1.110  
   1.111    \noindent The theory sources should be put into the @{verbatim Foo}
   1.112    directory, and its @{verbatim ROOT.ML} should be edited to load all
   1.113 -  required theories.  Invoking @{verbatim isatool} @{tool make} again
   1.114 +  required theories.  Invoking @{verbatim isabelle} @{tool make} again
   1.115    would run the whole session, generating browser information and the
   1.116    document automatically.  The @{verbatim IsaMakefile} is typically
   1.117    tuned manually later, e.g.\ adding source dependencies, or changing
   1.118 @@ -423,7 +423,7 @@
   1.119    meant to cover all of the sub-session directories at the same time
   1.120    (this is the deeper reasong why @{verbatim IsaMakefile} is not made
   1.121    part of the initial session directory created by @{verbatim
   1.122 -  isatool} @{tool mkdir}).  See @{"file" "~~/src/HOL/IsaMakefile"} for
   1.123 +  isabelle} @{tool mkdir}).  See @{"file" "~~/src/HOL/IsaMakefile"} for
   1.124    a full-blown example.
   1.125  *}
   1.126  
   1.127 @@ -546,10 +546,10 @@
   1.128    relative to the session's main directory.  If the @{verbatim "-C"}
   1.129    option is true, this will include a copy of an existing @{verbatim
   1.130    document} directory as provided by the user.  For example,
   1.131 -  @{verbatim isatool} @{tool usedir}~@{verbatim "-D generated HOL
   1.132 +  @{verbatim isabelle} @{tool usedir}~@{verbatim "-D generated HOL
   1.133    Foo"} produces a complete set of document sources at @{verbatim
   1.134    "Foo/generated"}.  Subsequent invocation of @{verbatim
   1.135 -  isatool} @{tool document}~@{verbatim "Foo/generated"} (see also
   1.136 +  isabelle} @{tool document}~@{verbatim "Foo/generated"} (see also
   1.137    \secref{sec:tool-document}) will process the final result
   1.138    independently of an Isabelle job.  This decoupled mode of operation
   1.139    facilitates debugging of serious {\LaTeX} errors, for example.
   1.140 @@ -697,7 +697,7 @@
   1.141    "~~/lib/texinputs/pdfsetup.sty"} as well.
   1.142  
   1.143    \medskip As a final step of document preparation within Isabelle,
   1.144 -  @{verbatim isatool} @{tool document}~@{verbatim "-c"} is run on the
   1.145 +  @{verbatim isabelle} @{tool document}~@{verbatim "-c"} is run on the
   1.146    resulting @{verbatim document} directory.  Thus the actual output
   1.147    document is built and installed in its proper place (as linked by
   1.148    the session's @{verbatim index.html} if option @{verbatim "-i"} of
   1.149 @@ -748,7 +748,7 @@
   1.150  subsubsection {* Examples *}
   1.151  
   1.152  text {*
   1.153 -  Invoking @{verbatim isatool} @{tool latex} by hand may be
   1.154 +  Invoking @{verbatim isabelle} @{tool latex} by hand may be
   1.155    occasionally useful when debugging failed attempts of the automatic
   1.156    document preparation stage of batch-mode Isabelle.  The abortive
   1.157    process leaves the sources at a certain place within @{setting
   1.158 @@ -757,7 +757,7 @@
   1.159    like this:
   1.160  \begin{ttbox}
   1.161    cd ~/isabelle/browser_info/HOL/Test/document
   1.162 -  isatool latex -o pdf
   1.163 +  isabelle latex -o pdf
   1.164  \end{ttbox}
   1.165  *}
   1.166