# HG changeset patch # User wenzelm # Date 1430947689 -7200 # Node ID a147272b16f9bbf6181668f5ef442b49f0489c33 # Parent 652a8e72cb75c9b4dd0dbe1a8551fa7ad24e43c8 tuned; diff -r 652a8e72cb75 -r a147272b16f9 src/Doc/Implementation/Integration.thy --- a/src/Doc/Implementation/Integration.thy Wed May 06 23:11:01 2015 +0200 +++ b/src/Doc/Implementation/Integration.thy Wed May 06 23:28:09 2015 +0200 @@ -187,7 +187,7 @@ sub-graph of theories, the intrinsic parallelism can be exploited by the system to speedup loading. - This variant is used by default in @{tool build} @{cite "isabelle-sys"}. + This variant is used by default in @{tool build} @{cite "isabelle-system"}. \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value presently associated with name @{text A}. Note that the result might be diff -r 652a8e72cb75 -r a147272b16f9 src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Wed May 06 23:11:01 2015 +0200 +++ b/src/Doc/Implementation/ML.thy Wed May 06 23:28:09 2015 +0200 @@ -1418,7 +1418,7 @@ \item sequence of Isabelle symbols (see also \secref{sec:symbols}), with @{ML Symbol.explode} as key operation; - \item XML tree structure via YXML (see also @{cite "isabelle-sys"}), + \item XML tree structure via YXML (see also @{cite "isabelle-system"}), with @{ML YXML.parse_body} as key operation. \end{enumerate} diff -r 652a8e72cb75 -r a147272b16f9 src/Doc/Isar_Ref/Document_Preparation.thy --- a/src/Doc/Isar_Ref/Document_Preparation.thy Wed May 06 23:11:01 2015 +0200 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy Wed May 06 23:28:09 2015 +0200 @@ -11,7 +11,7 @@ {\LaTeX} output is generated while processing a \emph{session} in batch mode, as explained in the \emph{The Isabelle System Manual} - @{cite "isabelle-sys"}. The main Isabelle tools to get started with + @{cite "isabelle-system"}. The main Isabelle tools to get started with document preparation are @{tool_ref mkroot} and @{tool_ref build}. The classic Isabelle/HOL tutorial @{cite "isabelle-hol-book"} also @@ -434,7 +434,7 @@ \end{tabular} \medskip The Isabelle document preparation system - @{cite "isabelle-sys"} allows tagged command regions to be presented + @{cite "isabelle-system"} allows tagged command regions to be presented specifically, e.g.\ to fold proof texts, or drop parts of the text completely. @@ -459,7 +459,7 @@ arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding parts of the text. Logic sessions may also specify ``document versions'', where given tags are interpreted in some particular way. - Again see @{cite "isabelle-sys"} for further details. + Again see @{cite "isabelle-system"} for further details. \ diff -r 652a8e72cb75 -r a147272b16f9 src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Wed May 06 23:11:01 2015 +0200 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Wed May 06 23:28:09 2015 +0200 @@ -110,7 +110,7 @@ @{command "print_state"}~@{text "(latex xsymbols)"} prints the current proof state with mathematical symbols and special characters represented in {\LaTeX} source, according to the Isabelle style - @{cite "isabelle-sys"}. + @{cite "isabelle-system"}. Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more systematic way to include formal items into the printed text diff -r 652a8e72cb75 -r a147272b16f9 src/Doc/Isar_Ref/Misc.thy --- a/src/Doc/Isar_Ref/Misc.thy Wed May 06 23:11:01 2015 +0200 +++ b/src/Doc/Isar_Ref/Misc.thy Wed May 06 23:28:09 2015 +0200 @@ -103,7 +103,7 @@ \item @{command "thm_deps"}~@{text "a\<^sub>1 \ a\<^sub>n"} visualizes dependencies of facts, using Isabelle's graph browser - tool (see also @{cite "isabelle-sys"}). + tool (see also @{cite "isabelle-system"}). \item @{command "unused_thms"}~@{text "A\<^sub>1 \ A\<^sub>m - B\<^sub>1 \ B\<^sub>n"} displays all theorems that are proved in theories @{text "B\<^sub>1 \ B\<^sub>n"} diff -r 652a8e72cb75 -r a147272b16f9 src/Doc/Isar_Ref/Outer_Syntax.thy --- a/src/Doc/Isar_Ref/Outer_Syntax.thy Wed May 06 23:11:01 2015 +0200 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Wed May 06 23:28:09 2015 +0200 @@ -28,7 +28,7 @@ Printed theory documents usually omit quotes to gain readability (this is a matter of {\LaTeX} macro setup, say via @{verbatim - "\\isabellestyle"}, see also @{cite "isabelle-sys"}). Experienced + "\\isabellestyle"}, see also @{cite "isabelle-system"}). Experienced users of Isabelle/Isar may easily reconstruct the lost technical information, while mere readers need not care about quotes at all. \ diff -r 652a8e72cb75 -r a147272b16f9 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Wed May 06 23:11:01 2015 +0200 +++ b/src/Doc/JEdit/JEdit.thy Wed May 06 23:28:09 2015 +0200 @@ -82,7 +82,7 @@ The options allow to specify a logic session name --- the same selector is accessible in the \emph{Theories} panel (\secref{sec:theories}). On application startup, the selected logic session image is provided - automatically by the Isabelle build tool @{cite "isabelle-sys"}: if it is + automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is absent or outdated wrt.\ its sources, the build process updates it before entering the Prover IDE. Change of the logic session within Isabelle/jEdit requires a restart of the whole application. @@ -170,7 +170,7 @@ Isabelle system options are managed by Isabelle/Scala and changes are stored in @{file_unchecked "$ISABELLE_HOME_USER/etc/preferences"}, independently of - other jEdit properties. See also @{cite "isabelle-sys"}, especially the + other jEdit properties. See also @{cite "isabelle-system"}, especially the coverage of sessions and command-line tools like @{tool build} or @{tool options}. @@ -182,7 +182,7 @@ Isabelle system options. Note that some of these options affect general parameters that are relevant outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or @{system_option parallel_proofs} for the - Isabelle build tool @{cite "isabelle-sys"}, but it is possible to use the + Isabelle build tool @{cite "isabelle-system"}, but it is possible to use the settings variable @{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds without affecting Isabelle/jEdit. @@ -243,7 +243,7 @@ The @{verbatim "-l"} option specifies the session name of the logic image to be used for proof processing. Additional session root directories may be included via option @{verbatim "-d"} to augment - that name space of @{tool build} @{cite "isabelle-sys"}. + that name space of @{tool build} @{cite "isabelle-system"}. By default, the specified image is checked and built on demand. The @{verbatim "-s"} option determines where to store the result session image @@ -257,7 +257,7 @@ The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass additional low-level options to the JVM or jEdit, respectively. The defaults are - provided by the Isabelle settings environment @{cite "isabelle-sys"}, but + provided by the Isabelle settings environment @{cite "isabelle-system"}, but note that these only work for the command-line tool described here, and not the regular application. @@ -699,7 +699,7 @@ The \emph{Theories} panel (see also \figref{fig:theories}) provides an overview of the status of continuous checking of theory nodes within the document model. Unlike batch sessions of @{tool build} @{cite - "isabelle-sys"}, theory nodes are identified by full path names; this allows + "isabelle-system"}, theory nodes are identified by full path names; this allows to work with multiple (disjoint) Isabelle sessions simultaneously within the same editor session. @@ -1576,7 +1576,7 @@ text \The ultimate purpose of Isabelle is to produce nicely rendered documents with the Isabelle document preparation system, which is based on {\LaTeX}; - see also @{cite "isabelle-sys" and "isabelle-isar-ref"}. Isabelle/jEdit + see also @{cite "isabelle-system" and "isabelle-isar-ref"}. Isabelle/jEdit provides some additional support for document editing.\ @@ -1607,7 +1607,7 @@ text \Citations are managed by {\LaTeX} and Bib{\TeX} in @{verbatim ".bib"} files. The Isabelle session build process and the @{tool latex} tool @{cite - "isabelle-sys"} are smart enough to assemble the result, based on the + "isabelle-system"} are smart enough to assemble the result, based on the session directory layout. The document antiquotation @{text "@{cite}"} is described in @{cite diff -r 652a8e72cb75 -r a147272b16f9 src/Doc/Tutorial/Documents/Documents.thy --- a/src/Doc/Tutorial/Documents/Documents.thy Wed May 06 23:11:01 2015 +0200 +++ b/src/Doc/Tutorial/Documents/Documents.thy Wed May 06 23:28:09 2015 +0200 @@ -345,7 +345,7 @@ setup) and \texttt{isabelle build} (to run sessions as specified in the corresponding \texttt{ROOT} file). These Isabelle tools are described in further detail in the \emph{Isabelle System Manual} - @{cite "isabelle-sys"}. + @{cite "isabelle-system"}. For example, a new session \texttt{MySession} (with document preparation) may be produced as follows: @@ -406,7 +406,7 @@ \texttt{MySession/document} directory as well. In particular, adding a file named \texttt{root.bib} causes an automatic run of \texttt{bibtex} to process a bibliographic database; see also - \texttt{isabelle document} @{cite "isabelle-sys"}. + \texttt{isabelle document} @{cite "isabelle-system"}. \medskip Any failure of the document preparation phase in an Isabelle batch session leaves the generated sources in their target @@ -694,7 +694,7 @@ preparation system allows the user to specify how to interpret a tagged region, in order to keep, drop, or fold the corresponding parts of the document. See the \emph{Isabelle System Manual} - @{cite "isabelle-sys"} for further details, especially on + @{cite "isabelle-system"} for further details, especially on \texttt{isabelle build} and \texttt{isabelle document}. Ignored material is specified by delimiting the original formal diff -r 652a8e72cb75 -r a147272b16f9 src/Doc/manual.bib --- a/src/Doc/manual.bib Wed May 06 23:11:01 2015 +0200 +++ b/src/Doc/manual.bib Wed May 06 23:28:09 2015 +0200 @@ -1826,7 +1826,7 @@ title = "{SPASS} Version 3.5", note = {\url{http://www.spass-prover.org/publications/spass.pdf}}} -@manual{isabelle-sys, +@manual{isabelle-system, author = {Makarius Wenzel and Stefan Berghofer}, title = {The {Isabelle} System Manual}, institution = {TU Munich},