--- a/src/Doc/Implementation/Eq.thy Sun Oct 05 22:46:20 2014 +0200
+++ b/src/Doc/Implementation/Eq.thy Sun Oct 05 22:47:07 2014 +0200
@@ -76,7 +76,7 @@
%FIXME
The classic article that introduces the concept of conversion (for
- Cambridge LCF) is \cite{paulson:1983}.
+ Cambridge LCF) is @{cite "paulson:1983"}.
*}
--- a/src/Doc/Implementation/Integration.thy Sun Oct 05 22:46:20 2014 +0200
+++ b/src/Doc/Implementation/Integration.thy Sun Oct 05 22:47:07 2014 +0200
@@ -15,7 +15,8 @@
stateless manner. Historically, the sequence of transitions was wrapped up
as sequential command loop, such that commands are applied one-by-one. In
contemporary Isabelle/Isar, processing toplevel commands usually works in
- parallel in multi-threaded Isabelle/ML \cite{Wenzel:2009,Wenzel:2013:ITP}.
+ parallel in multi-threaded Isabelle/ML @{cite "Wenzel:2009" and
+ "Wenzel:2013:ITP"}.
*}
@@ -182,7 +183,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-sys"}.
\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/Isar.thy Sun Oct 05 22:46:20 2014 +0200
+++ b/src/Doc/Implementation/Isar.thy Sun Oct 05 22:47:07 2014 +0200
@@ -5,7 +5,7 @@
chapter {* Isar language elements *}
text {* The Isar proof language (see also
- \cite[\S2]{isabelle-isar-ref}) consists of three main categories of
+ @{cite \<open>\S2\<close> "isabelle-isar-ref"}) consists of three main categories of
language elements:
\begin{enumerate}
@@ -96,7 +96,7 @@
unless a certain linguistic mode is active, namely ``@{text
"proof(state)"}'', ``@{text "proof(chain)"}'', ``@{text
"proof(prove)"}'', respectively (using the terminology of
- \cite{isabelle-isar-ref}).
+ @{cite "isabelle-isar-ref"}).
It is advisable study the implementations of existing proof commands
for suitable modes to be asserted.
@@ -351,7 +351,7 @@
*}
text %mlex {* See also @{command method_setup} in
- \cite{isabelle-isar-ref} which includes some abstract examples.
+ @{cite "isabelle-isar-ref"} which includes some abstract examples.
\medskip The following toy examples illustrate how the goal facts
and state are passed to proof methods. The predefined proof method
@@ -394,7 +394,7 @@
The @{ML Attrib.thms} parser produces a list of theorems from the
usual Isar syntax involving attribute expressions etc.\ (syntax
- category @{syntax thmrefs}) \cite{isabelle-isar-ref}. The resulting
+ category @{syntax thmrefs}) @{cite "isabelle-isar-ref"}. The resulting
@{ML_text thms} are added to @{ML HOL_basic_ss} which already
contains the basic Simplifier setup for HOL.
@@ -575,6 +575,6 @@
*}
text %mlex {* See also @{command attribute_setup} in
- \cite{isabelle-isar-ref} which includes some abstract examples. *}
+ @{cite "isabelle-isar-ref"} which includes some abstract examples. *}
end
--- a/src/Doc/Implementation/Local_Theory.thy Sun Oct 05 22:46:20 2014 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy Sun Oct 05 22:47:07 2014 +0200
@@ -90,7 +90,7 @@
reset to the target context. The target now holds definitions for
terms and theorems that stem from the hypothetical @{text
"\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by the
- particular target policy (see \cite[\S4--5]{Haftmann-Wenzel:2009}
+ particular target policy (see @{cite \<open>\S4--5\<close> "Haftmann-Wenzel:2009"}
for details). *}
text %mlref {*
@@ -159,7 +159,7 @@
text {*
%FIXME
- See also \cite{Chaieb-Wenzel:2007}.
+ See also @{cite "Chaieb-Wenzel:2007"}.
*}
end
--- a/src/Doc/Implementation/Logic.thy Sun Oct 05 22:46:20 2014 +0200
+++ b/src/Doc/Implementation/Logic.thy Sun Oct 05 22:47:07 2014 +0200
@@ -7,9 +7,9 @@
text {*
The logical foundations of Isabelle/Isar are that of the Pure logic,
which has been introduced as a Natural Deduction framework in
- \cite{paulson700}. This is essentially the same logic as ``@{text
+ @{cite paulson700}. This is essentially the same logic as ``@{text
"\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS)
- \cite{Barendregt-Geuvers:2001}, although there are some key
+ @{cite "Barendregt-Geuvers:2001"}, although there are some key
differences in the specific treatment of simple types in
Isabelle/Pure.
@@ -112,7 +112,7 @@
\<alpha>\<^bsub>s\<^sub>k\<^esub>)\<kappa>"} is of sort @{text "s"}.
Consequently, type unification has most general solutions (modulo
equivalence of sorts), so type-inference produces primary types as
- expected \cite{nipkow-prehofer}.
+ expected @{cite "nipkow-prehofer"}.
*}
text %mlref {*
@@ -237,8 +237,8 @@
text {*
The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
- with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
- or \cite{paulson-ml2}), with the types being determined by the
+ with de-Bruijn indices for bound variables (cf.\ @{cite debruijn72}
+ or @{cite "paulson-ml2"}), with the types being determined by the
corresponding binders. In contrast, free variables and constants
have an explicit name and type in each occurrence.
@@ -558,7 +558,7 @@
explicit proof terms for primitive inferences, see also
\secref{sec:proof-terms}. Thus all three levels of @{text
"\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for terms, and @{text
- "\<And>/\<Longrightarrow>"} for proofs (cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}).
+ "\<And>/\<Longrightarrow>"} for proofs (cf.\ @{cite "Berghofer-Nipkow:2000:TPHOL"}).
Observe that locally fixed parameters (as in @{text
"\<And>\<hyphen>intro"}) need not be recorded in the hypotheses, because
@@ -566,7 +566,7 @@
``Assumptions'' @{text "x :: \<tau>"} for type-membership are only
present as long as some @{text "x\<^sub>\<tau>"} occurs in the statement
body.\footnote{This is the key difference to ``@{text "\<lambda>HOL"}'' in
- the PTS framework \cite{Barendregt-Geuvers:2001}, where hypotheses
+ the PTS framework @{cite "Barendregt-Geuvers:2001"}, where hypotheses
@{text "x : A"} are treated uniformly for propositions and types.}
\medskip The axiomatization of a theory is implicitly closed by
@@ -628,7 +628,7 @@
"d(\<alpha>\<^sub>i)"} for some @{text "\<alpha>\<^sub>i"} projected from @{text
"\<^vec>\<alpha>"}. Thus overloaded definitions essentially work by
primitive recursion over the syntactic structure of a single type
- argument. See also \cite[\S4.3]{Haftmann-Wenzel:2006:classes}.
+ argument. See also @{cite \<open>\S4.3\<close> "Haftmann-Wenzel:2006:classes"}.
*}
text %mlref {*
@@ -1009,8 +1009,8 @@
text {*
The idea of object-level rules is to model Natural Deduction
- inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow
- arbitrary nesting similar to \cite{extensions91}. The most basic
+ inferences in the style of Gentzen @{cite "Gentzen:1935"}, but we allow
+ arbitrary nesting similar to @{cite extensions91}. The most basic
rule format is that of a \emph{Horn Clause}:
\[
\infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\<dots>"} & @{text "A\<^sub>n"}}
@@ -1033,7 +1033,7 @@
Nesting of rules means that the positions of @{text "A\<^sub>i"} may
again hold compound rules, not just atomic propositions.
Propositions of this format are called \emph{Hereditary Harrop
- Formulae} in the literature \cite{Miller:1991}. Here we give an
+ Formulae} in the literature @{cite "Miller:1991"}. Here we give an
inductive characterization as follows:
\medskip
@@ -1222,7 +1222,7 @@
according to the propositions-as-types principle. The resulting
3-level @{text "\<lambda>"}-calculus resembles ``@{text "\<lambda>HOL"}'' in the
more abstract setting of Pure Type Systems (PTS)
- \cite{Barendregt-Geuvers:2001}, if some fine points like schematic
+ @{cite "Barendregt-Geuvers:2001"}, if some fine points like schematic
polymorphism and type classes are ignored.
\medskip\emph{Proof abstractions} of the form @{text "\<^bold>\<lambda>x :: \<alpha>. prf"}
@@ -1284,7 +1284,7 @@
There are separate operations to reconstruct the full proof term
later on, using \emph{higher-order pattern unification}
- \cite{nipkow-patterns,Berghofer-Nipkow:2000:TPHOL}.
+ @{cite "nipkow-patterns" and "Berghofer-Nipkow:2000:TPHOL"}.
The \emph{proof checker} expects a fully reconstructed proof term,
and can turn it into a theorem by replaying its primitive inferences
@@ -1294,7 +1294,7 @@
subsection {* Concrete syntax of proof terms *}
text {* The concrete syntax of proof terms is a slight extension of
- the regular inner syntax of Isabelle/Pure \cite{isabelle-isar-ref}.
+ the regular inner syntax of Isabelle/Pure @{cite "isabelle-isar-ref"}.
Its main syntactic category @{syntax (inner) proof} is defined as
follows:
--- a/src/Doc/Implementation/ML.thy Sun Oct 05 22:46:20 2014 +0200
+++ b/src/Doc/Implementation/ML.thy Sun Oct 05 22:47:07 2014 +0200
@@ -681,7 +681,7 @@
\<close>}
Here @{syntax nameref} and @{syntax args} are outer syntax categories, as
- defined in \cite{isabelle-isar-ref}.
+ defined in @{cite "isabelle-isar-ref"}.
\medskip A regular antiquotation @{text "@{name args}"} processes
its arguments by the usual means of the Isar source language, and
@@ -1008,7 +1008,7 @@
batch sessions prefixes each line of warnings by @{verbatim
"###"} and errors by @{verbatim "***"}, but leaves anything else
unchanged. The message body may contain further markup and formatting,
- which is routinely used in the Prover IDE \cite{isabelle-jedit}.
+ which is routinely used in the Prover IDE @{cite "isabelle-jedit"}.
Messages are associated with the transaction context of the running
Isar command. This enables the front-end to manage commands and
@@ -1325,7 +1325,7 @@
\item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
"Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify standard
symbols according to fixed syntactic conventions of Isabelle, cf.\
- \cite{isabelle-isar-ref}.
+ @{cite "isabelle-isar-ref"}.
\item Type @{ML_type "Symbol.sym"} is a concrete datatype that
represents the different kinds of symbols explicitly, with
@@ -1404,7 +1404,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-sys"}),
with @{ML YXML.parse_body} as key operation.
\end{enumerate}
@@ -1686,15 +1686,15 @@
Law'' follows different rules: clock frequency has reached its peak
around 2005, and applications need to be parallelized in order to
avoid a perceived loss of performance. See also
- \cite{Sutter:2005}.}
+ @{cite "Sutter:2005"}.}
Isabelle/Isar exploits the inherent structure of theories and proofs to
support \emph{implicit parallelism} to a large extent. LCF-style theorem
proving provides almost ideal conditions for that, see also
- \cite{Wenzel:2009}. This means, significant parts of theory and proof
+ @{cite "Wenzel:2009"}. This means, significant parts of theory and proof
checking is parallelized by default. In Isabelle2013, a maximum
speedup-factor of 3.5 on 4 cores and 6.5 on 8 cores can be expected
- \cite{Wenzel:2013:ITP}.
+ @{cite "Wenzel:2013:ITP"}.
\medskip ML threads lack the memory protection of separate
processes, and operate concurrently on shared heap memory. This has
@@ -2156,11 +2156,11 @@
text {*
Futures help to organize parallel execution in a value-oriented manner, with
@{text fork}~/ @{text join} as the main pair of operations, and some further
- variants; see also \cite{Wenzel:2009,Wenzel:2013:ITP}. Unlike lazy values,
- futures are evaluated strictly and spontaneously on separate worker threads.
- Futures may be canceled, which leads to interrupts on running evaluation
- attempts, and forces structurally related futures to fail for all time;
- already finished futures remain unchanged. Exceptions between related
+ variants; see also @{cite "Wenzel:2009" and "Wenzel:2013:ITP"}. Unlike lazy
+ values, futures are evaluated strictly and spontaneously on separate worker
+ threads. Futures may be canceled, which leads to interrupts on running
+ evaluation attempts, and forces structurally related futures to fail for all
+ time; already finished futures remain unchanged. Exceptions between related
futures are propagated as well, and turned into parallel exceptions (see
above).
--- a/src/Doc/Implementation/Prelim.thy Sun Oct 05 22:46:20 2014 +0200
+++ b/src/Doc/Implementation/Prelim.thy Sun Oct 05 22:47:07 2014 +0200
@@ -58,7 +58,7 @@
elimination rules for arbitrary operators (depending on the
object-logic and application), which enables users to perform
standard proof steps implicitly (cf.\ the @{text "rule"} method
- \cite{isabelle-isar-ref}).
+ @{cite "isabelle-isar-ref"}).
\medskip Thus Isabelle/Isar is able to bring forth more and more
concepts successively. In particular, an object-logic like
--- a/src/Doc/Implementation/Proof.thy Sun Oct 05 22:46:20 2014 +0200
+++ b/src/Doc/Implementation/Proof.thy Sun Oct 05 22:47:07 2014 +0200
@@ -380,7 +380,7 @@
conclusion: the proof demonstrates that the context may be augmented
by parameters and assumptions, without affecting any conclusions
that do not mention these parameters. See also
- \cite{isabelle-isar-ref} for the user-level @{command obtain} and
+ @{cite "isabelle-isar-ref"} for the user-level @{command obtain} and
@{command guess} elements. Final results, which may not refer to
the parameters in the conclusion, need to exported explicitly into
the original context. *}
--- a/src/Doc/Implementation/Syntax.thy Sun Oct 05 22:46:20 2014 +0200
+++ b/src/Doc/Implementation/Syntax.thy Sun Oct 05 22:47:07 2014 +0200
@@ -12,13 +12,13 @@
additional means for reading and printing of terms and types. This
important add-on outside the logical core is called \emph{inner
syntax} in Isabelle jargon, as opposed to the \emph{outer syntax} of
- the theory and proof language \cite{isabelle-isar-ref}.
+ the theory and proof language @{cite "isabelle-isar-ref"}.
- For example, according to \cite{church40} quantifiers are represented as
+ For example, according to @{cite church40} quantifiers are represented as
higher-order constants @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow> bool"} such that @{text
"All (\<lambda>x::'a. B x)"} faithfully represents the idea that is displayed in
Isabelle as @{text "\<forall>x::'a. B x"} via @{keyword "binder"} notation.
- Moreover, type-inference in the style of Hindley-Milner \cite{hindleymilner}
+ Moreover, type-inference in the style of Hindley-Milner @{cite hindleymilner}
(and extensions) enables users to write @{text "\<forall>x. B x"} concisely, when
the type @{text "'a"} is already clear from the
context.\footnote{Type-inference taken to the extreme can easily confuse
@@ -133,9 +133,9 @@
\medskip Note that the string values that are passed in and out are
annotated by the system, to carry further markup that is relevant for the
- Prover IDE \cite{isabelle-jedit}. User code should neither compose its own
- input strings, nor try to analyze the output strings. Conceptually this is
- an abstract datatype, encoded as concrete string for historical reasons.
+ Prover IDE @{cite "isabelle-jedit"}. User code should neither compose its
+ own input strings, nor try to analyze the output strings. Conceptually this
+ is an abstract datatype, encoded as concrete string for historical reasons.
The standard way to provide the required position markup for input works via
the outer syntax parser wrapper @{ML Parse.inner_syntax}, which is already
@@ -161,9 +161,10 @@
declaratively via mixfix annotations. Moreover, there are \emph{syntax
translations} that can be augmented by the user, either declaratively via
@{command translations} or programmatically via @{command
- parse_translation}, @{command print_translation} \cite{isabelle-isar-ref}.
- The final scope-resolution is performed by the system, according to name
- spaces for types, term variables and constants determined by the context.
+ parse_translation}, @{command print_translation} @{cite
+ "isabelle-isar-ref"}. The final scope-resolution is performed by the system,
+ according to name spaces for types, term variables and constants determined
+ by the context.
*}
text %mlref {*
@@ -216,7 +217,7 @@
before pretty printing.
A typical add-on for the check/uncheck syntax layer is the @{command
- abbreviation} mechanism \cite{isabelle-isar-ref}. Here the user specifies
+ abbreviation} mechanism @{cite "isabelle-isar-ref"}. Here the user specifies
syntactic definitions that are managed by the system as polymorphic @{text
"let"} bindings. These are expanded during the @{text "check"} phase, and
contracted during the @{text "uncheck"} phase, without affecting the
@@ -230,7 +231,7 @@
constants according to the ``dictionary construction'' of its
logical foundation. This involves ``type improvement''
(specialization of slightly too general types) and replacement by
- certain locale parameters. See also \cite{Haftmann-Wenzel:2009}.
+ certain locale parameters. See also @{cite "Haftmann-Wenzel:2009"}.
*}
text %mlref {*