--- 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
--- 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}
--- 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.
\<close>
--- 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
--- 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 \<dots> 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 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"}
displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}
--- 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.
\<close>
--- 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 \<open>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.\<close>
@@ -1607,7 +1607,7 @@
text \<open>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
--- 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
--- 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},