updated generated files;
authorwenzelm
Mon Nov 29 11:27:39 2010 +0100 (2010-11-29)
changeset 408023cd23f676c5b
parent 40801 6cfacec435e6
child 40805 5a195f11ef46
updated generated files;
doc-src/IsarImplementation/Thy/document/Isar.tex
doc-src/IsarImplementation/Thy/document/ML.tex
doc-src/IsarImplementation/Thy/document/Tactic.tex
doc-src/IsarRef/Thy/document/Document_Preparation.tex
doc-src/IsarRef/Thy/document/HOL_Specific.tex
doc-src/IsarRef/Thy/document/Spec.tex
doc-src/System/Thy/document/Basics.tex
doc-src/System/Thy/document/Misc.tex
doc-src/System/Thy/document/Presentation.tex
     1.1 --- a/doc-src/IsarImplementation/Thy/document/Isar.tex	Mon Nov 29 11:22:40 2010 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/Isar.tex	Mon Nov 29 11:27:39 2010 +0100
     1.3 @@ -708,7 +708,7 @@
     1.4  \medskip Apart from explicit arguments, common proof methods
     1.5    typically work with a default configuration provided by the context.
     1.6    As a shortcut to rule management we use a cheap solution via functor
     1.7 -  \verb|Named_Thms| (see also \hyperlink{file.~~/src/Pure/Tools/named-thms.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}Tools{\isaliteral{2F}{\isacharslash}}named{\isaliteral{5F}{\isacharunderscore}}thms{\isaliteral{2E}{\isachardot}}ML}}}}).%
     1.8 +  \verb|Named_Thms| (see also \verb|~~/src/Pure/Tools/named_thms.ML|).%
     1.9  \end{isamarkuptext}%
    1.10  \isamarkuptrue%
    1.11  %
     2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Mon Nov 29 11:22:40 2010 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Mon Nov 29 11:27:39 2010 +0100
     2.3 @@ -89,7 +89,7 @@
     2.4  Isabelle source files have a certain standardized header
     2.5    format (with precise spacing) that follows ancient traditions
     2.6    reaching back to the earliest versions of the system by Larry
     2.7 -  Paulson.  See \hyperlink{file.~~/src/Pure/thm.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}thm{\isaliteral{2E}{\isachardot}}ML}}}}, for example.
     2.8 +  Paulson.  See \verb|~~/src/Pure/thm.ML|, for example.
     2.9  
    2.10    The header includes at least \verb|Title| and \verb|Author| entries, followed by a prose description of the purpose of
    2.11    the module.  The latter can range from a single line to several
    2.12 @@ -1645,7 +1645,7 @@
    2.13    integer type --- overloading of SML97 is disabled.
    2.14  
    2.15    Structure \verb|IntInf| of SML97 is obsolete and superseded by
    2.16 -  \verb|Int|.  Structure \verb|Integer| in \hyperlink{file.~~/src/Pure/General/integer.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}integer{\isaliteral{2E}{\isachardot}}ML}}}} provides some additional
    2.17 +  \verb|Int|.  Structure \verb|Integer| in \verb|~~/src/Pure/General/integer.ML| provides some additional
    2.18    operations.
    2.19  
    2.20    \end{description}%
    2.21 @@ -1730,7 +1730,7 @@
    2.22  \begin{isamarkuptext}%
    2.23  Apart from \verb|Option.map| most operations defined in
    2.24    structure \verb|Option| are alien to Isabelle/ML.  The
    2.25 -  operations shown above are defined in \hyperlink{file.~~/src/Pure/General/basics.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}basics{\isaliteral{2E}{\isachardot}}ML}}}}, among others.%
    2.26 +  operations shown above are defined in \verb|~~/src/Pure/General/basics.ML|, among others.%
    2.27  \end{isamarkuptext}%
    2.28  \isamarkuptrue%
    2.29  %
    2.30 @@ -1771,7 +1771,7 @@
    2.31  
    2.32    \item \verb|member|, \verb|insert|, \verb|remove|, \verb|update| treat
    2.33    lists as a set-like container that maintains the order of elements.
    2.34 -  See \hyperlink{file.~~/src/Pure/library.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}library{\isaliteral{2E}{\isachardot}}ML}}}} for the full specifications
    2.35 +  See \verb|~~/src/Pure/library.ML| for the full specifications
    2.36    (written in ML).  There are some further derived operations like
    2.37    \verb|union| or \verb|inter|.
    2.38  
    2.39 @@ -1877,7 +1877,7 @@
    2.40  
    2.41    This way of merging lists is typical for context data
    2.42    (\secref{sec:context-data}).  See also \verb|merge| as defined in
    2.43 -  \hyperlink{file.~~/src/Pure/library.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}library{\isaliteral{2E}{\isachardot}}ML}}}}.%
    2.44 +  \verb|~~/src/Pure/library.ML|.%
    2.45  \end{isamarkuptext}%
    2.46  \isamarkuptrue%
    2.47  %
    2.48 @@ -1921,7 +1921,7 @@
    2.49  
    2.50    Association lists are adequate as simple and light-weight
    2.51    implementation of finite mappings in many practical situations.  A
    2.52 -  more heavy-duty table structure is defined in \hyperlink{file.~~/src/Pure/General/table.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}table{\isaliteral{2E}{\isachardot}}ML}}}}; that version scales easily to
    2.53 +  more heavy-duty table structure is defined in \verb|~~/src/Pure/General/table.ML|; that version scales easily to
    2.54    thousands or millions of elements.%
    2.55  \end{isamarkuptext}%
    2.56  \isamarkuptrue%
    2.57 @@ -2290,7 +2290,7 @@
    2.58  
    2.59    \end{description}
    2.60  
    2.61 -  There are some further variants of the \verb|Synchronized.guarded_access| combinator, see \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}Concurrent{\isaliteral{2F}{\isacharslash}}synchronized{\isaliteral{2E}{\isachardot}}ML}}}} for details.%
    2.62 +  There are some further variants of the \verb|Synchronized.guarded_access| combinator, see \verb|~~/src/Pure/Concurrent/synchronized.ML| for details.%
    2.63  \end{isamarkuptext}%
    2.64  \isamarkuptrue%
    2.65  %
    2.66 @@ -2357,7 +2357,7 @@
    2.67  \endisadelimML
    2.68  %
    2.69  \begin{isamarkuptext}%
    2.70 -\medskip See \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}Concurrent{\isaliteral{2F}{\isacharslash}}mailbox{\isaliteral{2E}{\isachardot}}ML}}}} how
    2.71 +\medskip See \verb|~~/src/Pure/Concurrent/mailbox.ML| how
    2.72    to implement a mailbox as synchronized variable over a purely
    2.73    functional queue.%
    2.74  \end{isamarkuptext}%
     3.1 --- a/doc-src/IsarImplementation/Thy/document/Tactic.tex	Mon Nov 29 11:22:40 2010 +0100
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Mon Nov 29 11:27:39 2010 +0100
     3.3 @@ -222,7 +222,7 @@
     3.4  
     3.5    \item Type \verb|tactic| represents tactics.  The
     3.6    well-formedness conditions described above need to be observed.  See
     3.7 -  also \hyperlink{file.~~/src/Pure/General/seq.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}seq{\isaliteral{2E}{\isachardot}}ML}}}} for the underlying
     3.8 +  also \verb|~~/src/Pure/General/seq.ML| for the underlying
     3.9    implementation of lazy sequences.
    3.10  
    3.11    \item Type \verb|int -> tactic| represents tactics with
     4.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Nov 29 11:22:40 2010 +0100
     4.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Nov 29 11:27:39 2010 +0100
     4.3 @@ -95,7 +95,7 @@
     4.4    document generated from a theory.  Each markup command takes a
     4.5    single \hyperlink{syntax.text}{\mbox{\isa{text}}} argument, which is passed as argument to a
     4.6    corresponding {\LaTeX} macro.  The default macros provided by
     4.7 -  \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}lib{\isaliteral{2F}{\isacharslash}}texinputs{\isaliteral{2F}{\isacharslash}}isabelle{\isaliteral{2E}{\isachardot}}sty}}}} can be redefined according
     4.8 +  \verb|~~/lib/texinputs/isabelle.sty| can be redefined according
     4.9    to the needs of the underlying document and {\LaTeX} styles.
    4.10  
    4.11    Note that formal comments (\secref{sec:comments}) are similar to
    4.12 @@ -174,6 +174,7 @@
    4.13      \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isa{antiquotation} \\
    4.14      \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}} & : & \isa{antiquotation} \\
    4.15      \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}} & : & \isa{antiquotation} \\
    4.16 +    \indexdef{}{antiquotation}{file}\hypertarget{antiquotation.file}{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}} & : & \isa{antiquotation} \\
    4.17    \end{matharray}
    4.18  
    4.19    The overall content of an Isabelle/Isar theory may alternate between
    4.20 @@ -219,7 +220,8 @@
    4.21        'full_prf' options thmrefs |
    4.22        'ML' options name |
    4.23        'ML_type' options name |
    4.24 -      'ML_struct' options name
    4.25 +      'ML_struct' options name |
    4.26 +      'file' options name
    4.27      ;
    4.28      options: '[' (option * ',') ']'
    4.29      ;
    4.30 @@ -300,6 +302,9 @@
    4.31    \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML{\isaliteral{5F}{\isacharunderscore}}type\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ML{\isaliteral{5F}{\isacharunderscore}}struct\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} check text \isa{s} as ML value, type, and
    4.32    structure, respectively.  The source is printed verbatim.
    4.33  
    4.34 +  \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}file\ path{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} checks that \isa{{\isaliteral{22}{\isachardoublequote}}path{\isaliteral{22}{\isachardoublequote}}} refers to a
    4.35 +  file (or directory) and prints it verbatim.
    4.36 +
    4.37    \end{description}%
    4.38  \end{isamarkuptext}%
    4.39  \isamarkuptrue%
    4.40 @@ -466,7 +471,7 @@
    4.41  
    4.42    \medskip Command tags merely produce certain markup environments for
    4.43    type-setting.  The meaning of these is determined by {\LaTeX}
    4.44 -  macros, as defined in \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}lib{\isaliteral{2F}{\isacharslash}}texinputs{\isaliteral{2F}{\isacharslash}}isabelle{\isaliteral{2E}{\isachardot}}sty}}}} or
    4.45 +  macros, as defined in \verb|~~/lib/texinputs/isabelle.sty| or
    4.46    by the document author.  The Isabelle document preparation tools
    4.47    also provide some high-level options to specify the meaning of
    4.48    arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
     5.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 29 11:22:40 2010 +0100
     5.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Nov 29 11:27:39 2010 +0100
     5.3 @@ -897,7 +897,7 @@
     5.4    The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
     5.5    \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
     5.6    applications in confluence theory, lattice theory and projective
     5.7 -  geometry.  See \hyperlink{file.~~/src/HOL/ex/Coherent.thy}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}HOL{\isaliteral{2F}{\isacharslash}}ex{\isaliteral{2F}{\isacharslash}}Coherent{\isaliteral{2E}{\isachardot}}thy}}}} for some
     5.8 +  geometry.  See \verb|~~/src/HOL/ex/Coherent.thy| for some
     5.9    examples.%
    5.10  \end{isamarkuptext}%
    5.11  \isamarkuptrue%
     6.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Nov 29 11:22:40 2010 +0100
     6.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Nov 29 11:27:39 2010 +0100
     6.3 @@ -1203,7 +1203,7 @@
     6.4  
     6.5    \end{description}
     6.6  
     6.7 -  See \hyperlink{file.~~/src/HOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}HOL{\isaliteral{2F}{\isacharslash}}ex{\isaliteral{2F}{\isacharslash}}Iff{\isaliteral{5F}{\isacharunderscore}}Oracle{\isaliteral{2E}{\isachardot}}thy}}}} for a worked example of
     6.8 +  See \verb|~~/src/HOL/ex/Iff_Oracle.thy| for a worked example of
     6.9    defining a new primitive rule as oracle, and turning it into a proof
    6.10    method.%
    6.11  \end{isamarkuptext}%
     7.1 --- a/doc-src/System/Thy/document/Basics.tex	Mon Nov 29 11:22:40 2010 +0100
     7.2 +++ b/doc-src/System/Thy/document/Basics.tex	Mon Nov 29 11:27:39 2010 +0100
     7.3 @@ -71,7 +71,7 @@
     7.4    their shell startup scripts, before being able to actually run the
     7.5    program. Isabelle requires none such administrative chores of its
     7.6    end-users --- the executables can be invoked straight away.
     7.7 -  Occasionally, users would still want to put the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}bin}}}} directory into their shell's search path, but
     7.8 +  Occasionally, users would still want to put the \verb|$ISABELLE_HOME/bin| directory into their shell's search path, but
     7.9    this is not required.%
    7.10  \end{isamarkuptext}%
    7.11  \isamarkuptrue%
    7.12 @@ -98,9 +98,9 @@
    7.13    note that the Isabelle executables either have to be run from their
    7.14    original location in the distribution directory, or via the
    7.15    executable objects created by the \hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}} utility.  Symbolic
    7.16 -  links are admissible, but a plain copy of the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}bin}}}} files will not work!
    7.17 +  links are admissible, but a plain copy of the \verb|$ISABELLE_HOME/bin| files will not work!
    7.18  
    7.19 -  \item The file \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}etc{\isaliteral{2F}{\isacharslash}}settings}}}} is run as a
    7.20 +  \item The file \verb|$ISABELLE_HOME/etc/settings| is run as a
    7.21    \indexref{}{executable}{bash}\hyperlink{executable.bash}{\mbox{\isa{\isatt{bash}}}} shell script with the auto-export option for
    7.22    variables enabled.
    7.23    
    7.24 @@ -117,10 +117,10 @@
    7.25    before --- usually to something like \verb|$HOME/.isabelle/IsabelleXXXX|.
    7.26    
    7.27    Thus individual users may override the site-wide defaults.  See also
    7.28 -  file \hyperlink{file.$ISABELLE-HOME/etc/user-settings.sample}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}etc{\isaliteral{2F}{\isacharslash}}user{\isaliteral{2D}{\isacharminus}}settings{\isaliteral{2E}{\isachardot}}sample}}}} in the
    7.29 +  file \verb|$ISABELLE_HOME/etc/user-settings.sample| in the
    7.30    distribution.  Typically, a user settings file would contain only a
    7.31    few lines, just the assigments that are really changed.  One should
    7.32 -  definitely \emph{not} start with a full copy the basic \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}etc{\isaliteral{2F}{\isacharslash}}settings}}}}. This could cause very annoying
    7.33 +  definitely \emph{not} start with a full copy the basic \verb|$ISABELLE_HOME/etc/settings|. This could cause very annoying
    7.34    maintainance problems later, when the Isabelle installation is
    7.35    updated or changed otherwise.
    7.36    
    7.37 @@ -193,7 +193,7 @@
    7.38  
    7.39    \item[\indexdef{}{setting}{ISABELLE\_PROCESS}\hypertarget{setting.ISABELLE-PROCESS}{\hyperlink{setting.ISABELLE-PROCESS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PROCESS}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}, \hyperlink{setting.ISABELLE-TOOL}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}TOOL}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] are automatically set to the full path
    7.40    names of the \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}} and \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}} executables, respectively.  Thus other tools and scripts
    7.41 -  need not assume that the \hyperlink{file.$ISABELLE-HOME/bin}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}bin}}}} directory is
    7.42 +  need not assume that the \verb|$ISABELLE_HOME/bin| directory is
    7.43    on the current search path of the shell.
    7.44    
    7.45    \item[\indexdef{}{setting}{ISABELLE\_IDENTIFIER}\hypertarget{setting.ISABELLE-IDENTIFIER}{\hyperlink{setting.ISABELLE-IDENTIFIER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] refers
    7.46 @@ -202,7 +202,7 @@
    7.47    \item[\indexdef{}{setting}{ML\_SYSTEM}\hypertarget{setting.ML-SYSTEM}{\hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}}}, \indexdef{}{setting}{ML\_HOME}\hypertarget{setting.ML-HOME}{\hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}HOME}}}}},
    7.48    \indexdef{}{setting}{ML\_OPTIONS}\hypertarget{setting.ML-OPTIONS}{\hyperlink{setting.ML-OPTIONS}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}}, \indexdef{}{setting}{ML\_PLATFORM}\hypertarget{setting.ML-PLATFORM}{\hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}}}, \indexdef{}{setting}{ML\_IDENTIFIER}\hypertarget{setting.ML-IDENTIFIER}{\hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] specify the underlying ML system
    7.49    to be used for Isabelle.  There is only a fixed set of admissable
    7.50 -  \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}} names (see the \hyperlink{file.$ISABELLE-HOME/etc/settings}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}etc{\isaliteral{2F}{\isacharslash}}settings}}}} file of the distribution).
    7.51 +  \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}} names (see the \verb|$ISABELLE_HOME/etc/settings| file of the distribution).
    7.52    
    7.53    The actual compiler binary will be run from the directory \hyperlink{setting.ML-HOME}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}HOME}}}}, with \hyperlink{setting.ML-OPTIONS}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}} as first arguments on the
    7.54    command line.  The optional \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}} may specify the
    7.55 @@ -429,7 +429,7 @@
    7.56  
    7.57    \medskip The \verb|-W| option makes Isabelle enter a special
    7.58    process wrapper for interaction via the Isabelle/Scala layer, see
    7.59 -  also \hyperlink{file.~~/src/Pure/System/isabelle-process.scala}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}System{\isaliteral{2F}{\isacharslash}}isabelle{\isaliteral{5F}{\isacharunderscore}}process{\isaliteral{2E}{\isachardot}}scala}}}}.  The
    7.60 +  also \verb|~~/src/Pure/System/isabelle_process.scala|.  The
    7.61    protocol between the ML and JVM process is private to the
    7.62    implementation.
    7.63  
     8.1 --- a/doc-src/System/Thy/document/Misc.tex	Mon Nov 29 11:22:40 2010 +0100
     8.2 +++ b/doc-src/System/Thy/document/Misc.tex	Mon Nov 29 11:27:39 2010 +0100
     8.3 @@ -250,7 +250,7 @@
     8.4  \begin{isamarkuptext}%
     8.5  Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
     8.6    object-logics as a model for your own developments.  For example,
     8.7 -  see \hyperlink{file.~~/src/FOL/IsaMakefile}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}FOL{\isaliteral{2F}{\isacharslash}}IsaMakefile}}}}.%
     8.8 +  see \verb|~~/src/FOL/IsaMakefile|.%
     8.9  \end{isamarkuptext}%
    8.10  \isamarkuptrue%
    8.11  %
    8.12 @@ -363,8 +363,8 @@
    8.13    sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.  Markup chunks start
    8.14    with an empty sub-chunk, and a second empty sub-chunk indicates
    8.15    close of an element.  Any other non-empty chunk consists of plain
    8.16 -  text.  For example, see \hyperlink{file.~~/src/Pure/General/yxml.ML}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}yxml{\isaliteral{2E}{\isachardot}}ML}}}} or
    8.17 -  \hyperlink{file.~~/src/Pure/General/yxml.scala}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}Pure{\isaliteral{2F}{\isacharslash}}General{\isaliteral{2F}{\isacharslash}}yxml{\isaliteral{2E}{\isachardot}}scala}}}}.
    8.18 +  text.  For example, see \verb|~~/src/Pure/General/yxml.ML| or
    8.19 +  \verb|~~/src/Pure/General/yxml.scala|.
    8.20  
    8.21    YXML documents may be detected quickly by checking that the first
    8.22    two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.%
     9.1 --- a/doc-src/System/Thy/document/Presentation.tex	Mon Nov 29 11:22:40 2010 +0100
     9.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Mon Nov 29 11:27:39 2010 +0100
     9.3 @@ -96,14 +96,14 @@
     9.4  
     9.5    The easiest way to let Isabelle generate theory browsing information
     9.6    for existing sessions is to append ``\verb|-i true|'' to the
     9.7 -  \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}USEDIR{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}} before invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} (or \hyperlink{file.$ISABELLE-HOME/build}{\mbox{\isa{\isatt{{\isaliteral{24}{\isachardollar}}ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{2F}{\isacharslash}}build}}}}).  For
     9.8 +  \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}USEDIR{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}} before invoking \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} (or \verb|$ISABELLE_HOME/build|).  For
     9.9    example, add something like this to your Isabelle settings file
    9.10  
    9.11  \begin{ttbox}
    9.12  ISABELLE_USEDIR_OPTIONS="-i true"
    9.13  \end{ttbox}
    9.14  
    9.15 -  and then change into the \hyperlink{file.~~/src/FOL}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}FOL}}}} directory and run
    9.16 +  and then change into the \verb|~~/src/FOL| directory and run
    9.17    \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle|
    9.18    \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|.  The presentation output will appear
    9.19    in \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
    9.20 @@ -111,7 +111,7 @@
    9.21    \verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
    9.22    more explicit about such details.
    9.23  
    9.24 -  Many standard Isabelle sessions (such as \hyperlink{file.~~/src/HOL/ex}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}HOL{\isaliteral{2F}{\isacharslash}}ex}}}})
    9.25 +  Many standard Isabelle sessions (such as \verb|~~/src/HOL/ex|)
    9.26    also provide actual printable documents.  These are prepared
    9.27    automatically as well if enabled like this, using the \verb|-d| option
    9.28  \begin{ttbox}
    9.29 @@ -451,7 +451,7 @@
    9.30    manual editing of the generated \verb|IsaMakefile|, which is
    9.31    meant to cover all of the sub-session directories at the same time
    9.32    (this is the deeper reasong why \verb|IsaMakefile| is not made
    9.33 -  part of the initial session directory created by \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}).  See \hyperlink{file.~~/src/HOL/IsaMakefile}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}HOL{\isaliteral{2F}{\isacharslash}}IsaMakefile}}}} for
    9.34 +  part of the initial session directory created by \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}).  See \verb|~~/src/HOL/IsaMakefile| for
    9.35    a full-blown example.%
    9.36  \end{isamarkuptext}%
    9.37  \isamarkuptrue%
    9.38 @@ -621,7 +621,7 @@
    9.39  \begin{isamarkuptext}%
    9.40  Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
    9.41    object-logics as a model for your own developments.  For example,
    9.42 -  see \hyperlink{file.~~/src/FOL/IsaMakefile}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}FOL{\isaliteral{2F}{\isacharslash}}IsaMakefile}}}}.  The Isabelle \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool creates \verb|IsaMakefile|s with proper invocation
    9.43 +  see \verb|~~/src/FOL/IsaMakefile|.  The Isabelle \indexref{}{tool}{mkdir}\hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}} tool creates \verb|IsaMakefile|s with proper invocation
    9.44    of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} as well.%
    9.45  \end{isamarkuptext}%
    9.46  \isamarkuptrue%
    9.47 @@ -670,7 +670,7 @@
    9.48    fold text tagged as \isa{foo}.  The builtin default is equivalent
    9.49    to the tag specification ``\verb|+theory,+proof,+ML,+visible,-invisible|''; see also the {\LaTeX}
    9.50    macros \verb|\isakeeptag|, \verb|\isadroptag|, and
    9.51 -  \verb|\isafoldtag|, in \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}lib{\isaliteral{2F}{\isacharslash}}texinputs{\isaliteral{2F}{\isacharslash}}isabelle{\isaliteral{2E}{\isachardot}}sty}}}}.
    9.52 +  \verb|\isafoldtag|, in \verb|~~/lib/texinputs/isabelle.sty|.
    9.53  
    9.54    \medskip Document preparation requires a properly setup ``\verb|document|'' directory within the logic session sources.  This
    9.55    directory is supposed to contain all the files needed to produce the
    9.56 @@ -701,7 +701,7 @@
    9.57    containing all the theories.
    9.58  
    9.59    The {\LaTeX} versions of the theories require some macros defined in
    9.60 -  \hyperlink{file.~~/lib/texinputs/isabelle.sty}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}lib{\isaliteral{2F}{\isacharslash}}texinputs{\isaliteral{2F}{\isacharslash}}isabelle{\isaliteral{2E}{\isachardot}}sty}}}}.  Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
    9.61 +  \verb|~~/lib/texinputs/isabelle.sty|.  Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
    9.62    the underlying Isabelle \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} tool already includes an
    9.63    appropriate path specification for {\TeX} inputs.
    9.64  
    9.65 @@ -710,11 +710,11 @@
    9.66    contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, see \cite{isabelle-implementation} for a
    9.67    complete list of predefined Isabelle symbols.  Users may invent
    9.68    further symbols as well, just by providing {\LaTeX} macros in a
    9.69 -  similar fashion as in \hyperlink{file.~~/lib/texinputs/isabellesym.sty}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}lib{\isaliteral{2F}{\isacharslash}}texinputs{\isaliteral{2F}{\isacharslash}}isabellesym{\isaliteral{2E}{\isachardot}}sty}}}} of
    9.70 +  similar fashion as in \verb|~~/lib/texinputs/isabellesym.sty| of
    9.71    the distribution.
    9.72  
    9.73    For proper setup of DVI and PDF documents (with hyperlinks and
    9.74 -  bookmarks), we recommend to include \hyperlink{file.~~/lib/texinputs/pdfsetup.sty}{\mbox{\isa{\isatt{{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}lib{\isaliteral{2F}{\isacharslash}}texinputs{\isaliteral{2F}{\isacharslash}}pdfsetup{\isaliteral{2E}{\isachardot}}sty}}}} as well.
    9.75 +  bookmarks), we recommend to include \verb|~~/lib/texinputs/pdfsetup.sty| as well.
    9.76  
    9.77    \medskip As a final step of document preparation within Isabelle,
    9.78    \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|-c| is run on the