# HG changeset patch # User wenzelm # Date 1291026459 -3600 # Node ID 3cd23f676c5bb73bf15ac429f458a312f4d0d74e # Parent 6cfacec435e6e4818beacb118377374fab08a44d updated generated files; diff -r 6cfacec435e6 -r 3cd23f676c5b doc-src/IsarImplementation/Thy/document/Isar.tex --- a/doc-src/IsarImplementation/Thy/document/Isar.tex Mon Nov 29 11:22:40 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Isar.tex Mon Nov 29 11:27:39 2010 +0100 @@ -708,7 +708,7 @@ \medskip Apart from explicit arguments, common proof methods typically work with a default configuration provided by the context. As a shortcut to rule management we use a cheap solution via functor - \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}}}}).% + \verb|Named_Thms| (see also \verb|~~/src/Pure/Tools/named_thms.ML|).% \end{isamarkuptext}% \isamarkuptrue% % diff -r 6cfacec435e6 -r 3cd23f676c5b doc-src/IsarImplementation/Thy/document/ML.tex --- a/doc-src/IsarImplementation/Thy/document/ML.tex Mon Nov 29 11:22:40 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Mon Nov 29 11:27:39 2010 +0100 @@ -89,7 +89,7 @@ Isabelle source files have a certain standardized header format (with precise spacing) that follows ancient traditions reaching back to the earliest versions of the system by Larry - 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. + Paulson. See \verb|~~/src/Pure/thm.ML|, for example. The header includes at least \verb|Title| and \verb|Author| entries, followed by a prose description of the purpose of the module. The latter can range from a single line to several @@ -1645,7 +1645,7 @@ integer type --- overloading of SML97 is disabled. Structure \verb|IntInf| of SML97 is obsolete and superseded by - \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 + \verb|Int|. Structure \verb|Integer| in \verb|~~/src/Pure/General/integer.ML| provides some additional operations. \end{description}% @@ -1730,7 +1730,7 @@ \begin{isamarkuptext}% Apart from \verb|Option.map| most operations defined in structure \verb|Option| are alien to Isabelle/ML. The - 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.% + operations shown above are defined in \verb|~~/src/Pure/General/basics.ML|, among others.% \end{isamarkuptext}% \isamarkuptrue% % @@ -1771,7 +1771,7 @@ \item \verb|member|, \verb|insert|, \verb|remove|, \verb|update| treat lists as a set-like container that maintains the order of elements. - 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 + See \verb|~~/src/Pure/library.ML| for the full specifications (written in ML). There are some further derived operations like \verb|union| or \verb|inter|. @@ -1877,7 +1877,7 @@ This way of merging lists is typical for context data (\secref{sec:context-data}). See also \verb|merge| as defined in - \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}}}}.% + \verb|~~/src/Pure/library.ML|.% \end{isamarkuptext}% \isamarkuptrue% % @@ -1921,7 +1921,7 @@ Association lists are adequate as simple and light-weight implementation of finite mappings in many practical situations. A - 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 + more heavy-duty table structure is defined in \verb|~~/src/Pure/General/table.ML|; that version scales easily to thousands or millions of elements.% \end{isamarkuptext}% \isamarkuptrue% @@ -2290,7 +2290,7 @@ \end{description} - 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.% + There are some further variants of the \verb|Synchronized.guarded_access| combinator, see \verb|~~/src/Pure/Concurrent/synchronized.ML| for details.% \end{isamarkuptext}% \isamarkuptrue% % @@ -2357,7 +2357,7 @@ \endisadelimML % \begin{isamarkuptext}% -\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 +\medskip See \verb|~~/src/Pure/Concurrent/mailbox.ML| how to implement a mailbox as synchronized variable over a purely functional queue.% \end{isamarkuptext}% diff -r 6cfacec435e6 -r 3cd23f676c5b doc-src/IsarImplementation/Thy/document/Tactic.tex --- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Mon Nov 29 11:22:40 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Mon Nov 29 11:27:39 2010 +0100 @@ -222,7 +222,7 @@ \item Type \verb|tactic| represents tactics. The well-formedness conditions described above need to be observed. See - 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 + also \verb|~~/src/Pure/General/seq.ML| for the underlying implementation of lazy sequences. \item Type \verb|int -> tactic| represents tactics with diff -r 6cfacec435e6 -r 3cd23f676c5b doc-src/IsarRef/Thy/document/Document_Preparation.tex --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon Nov 29 11:22:40 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Mon Nov 29 11:27:39 2010 +0100 @@ -95,7 +95,7 @@ document generated from a theory. Each markup command takes a single \hyperlink{syntax.text}{\mbox{\isa{text}}} argument, which is passed as argument to a corresponding {\LaTeX} macro. The default macros provided by - \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 + \verb|~~/lib/texinputs/isabelle.sty| can be redefined according to the needs of the underlying document and {\LaTeX} styles. Note that formal comments (\secref{sec:comments}) are similar to @@ -174,6 +174,7 @@ \indexdef{}{antiquotation}{ML}\hypertarget{antiquotation.ML}{\hyperlink{antiquotation.ML}{\mbox{\isa{ML}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{ML\_type}\hypertarget{antiquotation.ML-type}{\hyperlink{antiquotation.ML-type}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}type}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{ML\_struct}\hypertarget{antiquotation.ML-struct}{\hyperlink{antiquotation.ML-struct}{\mbox{\isa{ML{\isaliteral{5F}{\isacharunderscore}}struct}}}} & : & \isa{antiquotation} \\ + \indexdef{}{antiquotation}{file}\hypertarget{antiquotation.file}{\hyperlink{antiquotation.file}{\mbox{\isa{file}}}} & : & \isa{antiquotation} \\ \end{matharray} The overall content of an Isabelle/Isar theory may alternate between @@ -219,7 +220,8 @@ 'full_prf' options thmrefs | 'ML' options name | 'ML_type' options name | - 'ML_struct' options name + 'ML_struct' options name | + 'file' options name ; options: '[' (option * ',') ']' ; @@ -300,6 +302,9 @@ \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 structure, respectively. The source is printed verbatim. + \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 + file (or directory) and prints it verbatim. + \end{description}% \end{isamarkuptext}% \isamarkuptrue% @@ -466,7 +471,7 @@ \medskip Command tags merely produce certain markup environments for type-setting. The meaning of these is determined by {\LaTeX} - 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 + macros, as defined in \verb|~~/lib/texinputs/isabelle.sty| or by the document author. The Isabelle document preparation tools also provide some high-level options to specify the meaning of arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding diff -r 6cfacec435e6 -r 3cd23f676c5b doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Nov 29 11:22:40 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Nov 29 11:27:39 2010 +0100 @@ -897,7 +897,7 @@ The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers applications in confluence theory, lattice theory and projective - 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 + geometry. See \verb|~~/src/HOL/ex/Coherent.thy| for some examples.% \end{isamarkuptext}% \isamarkuptrue% diff -r 6cfacec435e6 -r 3cd23f676c5b doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Nov 29 11:22:40 2010 +0100 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Nov 29 11:27:39 2010 +0100 @@ -1203,7 +1203,7 @@ \end{description} - 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 + See \verb|~~/src/HOL/ex/Iff_Oracle.thy| for a worked example of defining a new primitive rule as oracle, and turning it into a proof method.% \end{isamarkuptext}% diff -r 6cfacec435e6 -r 3cd23f676c5b doc-src/System/Thy/document/Basics.tex --- a/doc-src/System/Thy/document/Basics.tex Mon Nov 29 11:22:40 2010 +0100 +++ b/doc-src/System/Thy/document/Basics.tex Mon Nov 29 11:27:39 2010 +0100 @@ -71,7 +71,7 @@ their shell startup scripts, before being able to actually run the program. Isabelle requires none such administrative chores of its end-users --- the executables can be invoked straight away. - 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 + Occasionally, users would still want to put the \verb|$ISABELLE_HOME/bin| directory into their shell's search path, but this is not required.% \end{isamarkuptext}% \isamarkuptrue% @@ -98,9 +98,9 @@ note that the Isabelle executables either have to be run from their original location in the distribution directory, or via the executable objects created by the \hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}} utility. Symbolic - 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! + links are admissible, but a plain copy of the \verb|$ISABELLE_HOME/bin| files will not work! - \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 + \item The file \verb|$ISABELLE_HOME/etc/settings| is run as a \indexref{}{executable}{bash}\hyperlink{executable.bash}{\mbox{\isa{\isatt{bash}}}} shell script with the auto-export option for variables enabled. @@ -117,10 +117,10 @@ before --- usually to something like \verb|$HOME/.isabelle/IsabelleXXXX|. Thus individual users may override the site-wide defaults. See also - 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 + file \verb|$ISABELLE_HOME/etc/user-settings.sample| in the distribution. Typically, a user settings file would contain only a few lines, just the assigments that are really changed. One should - 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 + definitely \emph{not} start with a full copy the basic \verb|$ISABELLE_HOME/etc/settings|. This could cause very annoying maintainance problems later, when the Isabelle installation is updated or changed otherwise. @@ -193,7 +193,7 @@ \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 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 - 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 + need not assume that the \verb|$ISABELLE_HOME/bin| directory is on the current search path of the shell. \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 @@ -202,7 +202,7 @@ \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}}}}}, \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 to be used for Isabelle. There is only a fixed set of admissable - \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). + \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}} names (see the \verb|$ISABELLE_HOME/etc/settings| file of the distribution). 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 command line. The optional \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}} may specify the @@ -429,7 +429,7 @@ \medskip The \verb|-W| option makes Isabelle enter a special process wrapper for interaction via the Isabelle/Scala layer, see - 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 + also \verb|~~/src/Pure/System/isabelle_process.scala|. The protocol between the ML and JVM process is private to the implementation. diff -r 6cfacec435e6 -r 3cd23f676c5b doc-src/System/Thy/document/Misc.tex --- a/doc-src/System/Thy/document/Misc.tex Mon Nov 29 11:22:40 2010 +0100 +++ b/doc-src/System/Thy/document/Misc.tex Mon Nov 29 11:27:39 2010 +0100 @@ -250,7 +250,7 @@ \begin{isamarkuptext}% Refer to the \verb|IsaMakefile|s of the Isabelle distribution's object-logics as a model for your own developments. For example, - 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}}}}.% + see \verb|~~/src/FOL/IsaMakefile|.% \end{isamarkuptext}% \isamarkuptrue% % @@ -363,8 +363,8 @@ sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}. Markup chunks start with an empty sub-chunk, and a second empty sub-chunk indicates close of an element. Any other non-empty chunk consists of plain - 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 - \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}}}}. + text. For example, see \verb|~~/src/Pure/General/yxml.ML| or + \verb|~~/src/Pure/General/yxml.scala|. YXML documents may be detected quickly by checking that the first two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.% diff -r 6cfacec435e6 -r 3cd23f676c5b doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Mon Nov 29 11:22:40 2010 +0100 +++ b/doc-src/System/Thy/document/Presentation.tex Mon Nov 29 11:27:39 2010 +0100 @@ -96,14 +96,14 @@ The easiest way to let Isabelle generate theory browsing information for existing sessions is to append ``\verb|-i true|'' to the - \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 + \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 example, add something like this to your Isabelle settings file \begin{ttbox} ISABELLE_USEDIR_OPTIONS="-i true" \end{ttbox} - 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 + and then change into the \verb|~~/src/FOL| directory and run \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|. The presentation output will appear in \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to @@ -111,7 +111,7 @@ \verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} more explicit about such details. - 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}}}}) + Many standard Isabelle sessions (such as \verb|~~/src/HOL/ex|) also provide actual printable documents. These are prepared automatically as well if enabled like this, using the \verb|-d| option \begin{ttbox} @@ -451,7 +451,7 @@ 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|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 + part of the initial session directory created by \verb|isabelle| \hyperlink{tool.mkdir}{\mbox{\isa{\isatt{mkdir}}}}). See \verb|~~/src/HOL/IsaMakefile| for a full-blown example.% \end{isamarkuptext}% \isamarkuptrue% @@ -621,7 +621,7 @@ \begin{isamarkuptext}% Refer to the \verb|IsaMakefile|s of the Isabelle distribution's object-logics as a model for your own developments. For example, - 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 + 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 of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} as well.% \end{isamarkuptext}% \isamarkuptrue% @@ -670,7 +670,7 @@ fold text tagged as \isa{foo}. The builtin default is equivalent to the tag specification ``\verb|+theory,+proof,+ML,+visible,-invisible|''; see also the {\LaTeX} macros \verb|\isakeeptag|, \verb|\isadroptag|, and - \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}}}}. + \verb|\isafoldtag|, in \verb|~~/lib/texinputs/isabelle.sty|. \medskip Document preparation requires a properly setup ``\verb|document|'' directory within the logic session sources. This directory is supposed to contain all the files needed to produce the @@ -701,7 +701,7 @@ containing all the theories. The {\LaTeX} versions of the theories require some macros 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}}}}. Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine; + \verb|~~/lib/texinputs/isabelle.sty|. Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine; the underlying Isabelle \hyperlink{tool.latex}{\mbox{\isa{\isatt{latex}}}} tool already includes an appropriate path specification for {\TeX} inputs. @@ -710,11 +710,11 @@ 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 complete list of predefined Isabelle symbols. Users may invent further symbols as well, just by providing {\LaTeX} macros in a - 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 + similar fashion as in \verb|~~/lib/texinputs/isabellesym.sty| of the distribution. For proper setup of DVI and PDF documents (with hyperlinks and - 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. + bookmarks), we recommend to include \verb|~~/lib/texinputs/pdfsetup.sty| as well. \medskip As a final step of document preparation within Isabelle, \verb|isabelle| \hyperlink{tool.document}{\mbox{\isa{\isatt{document}}}}~\verb|-c| is run on the