--- a/src/Doc/Classes/Classes.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Classes/Classes.thy Tue Oct 07 22:35:11 2014 +0200
@@ -5,7 +5,7 @@
section {* Introduction *}
text {*
- Type classes were introduced by Wadler and Blott \cite{wadler89how}
+ Type classes were introduced by Wadler and Blott @{cite wadler89how}
into the Haskell language to allow for a reasonable implementation
of overloading\footnote{throughout this tutorial, we are referring
to classical Haskell 1.0 type classes, not considering later
@@ -43,7 +43,7 @@
Indeed, type classes not only allow for simple overloading but form
a generic calculus, an instance of order-sorted algebra
- \cite{nipkow-sorts93,Nipkow-Prehofer:1993,Wenzel:1997:TPHOL}.
+ @{cite "nipkow-sorts93" and "Nipkow-Prehofer:1993" and "Wenzel:1997:TPHOL"}.
From a software engineering point of view, type classes roughly
correspond to interfaces in object-oriented languages like Java; so,
@@ -67,7 +67,7 @@
\noindent From a theoretical point of view, type classes are
lightweight modules; Haskell type classes may be emulated by SML
- functors \cite{classes_modules}. Isabelle/Isar offers a discipline
+ functors @{cite classes_modules}. Isabelle/Isar offers a discipline
of type classes which brings all those aspects together:
\begin{enumerate}
@@ -77,17 +77,17 @@
type
\item in connection with a ``less ad-hoc'' approach to overloading,
\item with a direct link to the Isabelle module system:
- locales \cite{kammueller-locales}.
+ locales @{cite "kammueller-locales"}.
\end{enumerate}
\noindent Isar type classes also directly support code generation in
a Haskell like fashion. Internally, they are mapped to more
- primitive Isabelle concepts \cite{Haftmann-Wenzel:2006:classes}.
+ primitive Isabelle concepts @{cite "Haftmann-Wenzel:2006:classes"}.
This tutorial demonstrates common elements of structured
specifications and abstract reasoning with type classes by the
algebraic hierarchy of semigroups, monoids and groups. Our
- background theory is that of Isabelle/HOL \cite{isa-tutorial}, for
+ background theory is that of Isabelle/HOL @{cite "isa-tutorial"}, for
which some familiarity is assumed.
*}
@@ -423,7 +423,7 @@
\noindent As you can see from this example, for local definitions
you may use any specification tool which works together with
locales, such as Krauss's recursive function package
- \cite{krauss2006}.
+ @{cite krauss2006}.
*}
@@ -583,7 +583,7 @@
overloading, it is obvious that overloading stemming from @{command
class} statements and @{command instantiation} targets naturally
maps to Haskell type classes. The code generator framework
- \cite{isabelle-codegen} takes this into account. If the target
+ @{cite "isabelle-codegen"} takes this into account. If the target
language (e.g.~SML) lacks type classes, then they are implemented by
an explicit dictionary construction. As example, let's go back to
the power function:
--- a/src/Doc/Codegen/Evaluation.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Codegen/Evaluation.thy Tue Oct 07 22:35:11 2014 +0200
@@ -53,7 +53,7 @@
subsubsection {* Normalization by evaluation (@{text nbe}) *}
text {*
- Normalization by evaluation \cite{Aehlig-Haftmann-Nipkow:2008:nbe}
+ Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"}
provides a comparably fast partially symbolic evaluation which
permits also normalization of functions and uninterpreted symbols;
the stack of code to be trusted is considerable.
--- a/src/Doc/Codegen/Further.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Codegen/Further.thy Tue Oct 07 22:35:11 2014 +0200
@@ -183,7 +183,7 @@
can be generated. But this not the case: internally, the term
@{text "fun_power.powers"} is an abbreviation for the foundational
term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
- (see \cite{isabelle-locale} for the details behind).
+ (see @{cite "isabelle-locale"} for the details behind).
Fortunately, with minor effort the desired behaviour can be
achieved. First, a dedicated definition of the constant on which
@@ -233,7 +233,7 @@
If you consider imperative data structures as inevitable for a
specific application, you should consider \emph{Imperative
Functional Programming with Isabelle/HOL}
- \cite{bulwahn-et-al:2008:imperative}; the framework described there
+ @{cite "bulwahn-et-al:2008:imperative"}; the framework described there
is available in session @{text Imperative_HOL}, together with a
short primer document.
*}
--- a/src/Doc/Codegen/Inductive_Predicate.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Codegen/Inductive_Predicate.thy Tue Oct 07 22:35:11 2014 +0200
@@ -23,7 +23,7 @@
which turns inductive specifications into equational ones, from
which in turn executable code can be generated. The mechanisms of
this compiler are described in detail in
- \cite{Berghofer-Bulwahn-Haftmann:2009:TPHOL}.
+ @{cite "Berghofer-Bulwahn-Haftmann:2009:TPHOL"}.
Consider the simple predicate @{const append} given by these two
introduction rules:
--- a/src/Doc/Codegen/Introduction.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Codegen/Introduction.thy Tue Oct 07 22:35:11 2014 +0200
@@ -8,12 +8,12 @@
This tutorial introduces the code generator facilities of @{text
"Isabelle/HOL"}. It allows to turn (a certain class of) HOL
specifications into corresponding executable code in the programming
- languages @{text SML} \cite{SML}, @{text OCaml} \cite{OCaml},
- @{text Haskell} \cite{haskell-revised-report} and @{text Scala}
- \cite{scala-overview-tech-report}.
+ languages @{text SML} @{cite SML}, @{text OCaml} @{cite OCaml},
+ @{text Haskell} @{cite "haskell-revised-report"} and @{text Scala}
+ @{cite "scala-overview-tech-report"}.
To profit from this tutorial, some familiarity and experience with
- @{theory HOL} \cite{isa-tutorial} and its basic theories is assumed.
+ @{theory HOL} @{cite "isa-tutorial"} and its basic theories is assumed.
*}
@@ -28,7 +28,7 @@
a generated program as an implementation of a higher-order rewrite
system, then every rewrite step performed by the program can be
simulated in the logic, which guarantees partial correctness
- \cite{Haftmann-Nipkow:2010:code}.
+ @{cite "Haftmann-Nipkow:2010:code"}.
*}
@@ -221,11 +221,11 @@
\item You may want to skim over the more technical sections
\secref{sec:adaptation} and \secref{sec:further}.
- \item The target language Scala \cite{scala-overview-tech-report}
+ \item The target language Scala @{cite "scala-overview-tech-report"}
comes with some specialities discussed in \secref{sec:scala}.
\item For exhaustive syntax diagrams etc. you should visit the
- Isabelle/Isar Reference Manual \cite{isabelle-isar-ref}.
+ Isabelle/Isar Reference Manual @{cite "isabelle-isar-ref"}.
\end{itemize}
--- a/src/Doc/Codegen/Refinement.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Codegen/Refinement.thy Tue Oct 07 22:35:11 2014 +0200
@@ -264,7 +264,7 @@
*}
text {*
- See further \cite{Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement}
+ See further @{cite "Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement"}
for the meta theory of datatype refinement involving invariants.
Typical data structures implemented by representations involving
--- a/src/Doc/Datatypes/Datatypes.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Oct 07 22:35:11 2014 +0200
@@ -23,7 +23,7 @@
text {*
The 2013 edition of Isabelle introduced a definitional package for freely
generated datatypes and codatatypes. This package replaces the earlier
-implementation due to Berghofer and Wenzel \cite{Berghofer-Wenzel:1999:TPHOL}.
+implementation due to Berghofer and Wenzel @{cite "Berghofer-Wenzel:1999:TPHOL"}.
Perhaps the main advantage of the new package is that it supports recursion
through a large class of non-datatypes, such as finite sets:
*}
@@ -80,13 +80,14 @@
\verb|~~/src/HOL/Library|.
The package, like its predecessor, fully adheres to the LCF philosophy
-\cite{mgordon79}: The characteristic theorems associated with the specified
+@{cite mgordon79}: The characteristic theorems associated with the specified
(co)datatypes are derived rather than introduced axiomatically.%
\footnote{However, some of the
internal constructions and most of the internal proof obligations are omitted
if the @{text quick_and_dirty} option is enabled.}
The package is described in a number of papers
-\cite{traytel-et-al-2012,blanchette-et-al-wit,blanchette-et-al-2014-impl,panny-et-al-2014}.
+@{cite "traytel-et-al-2012" and "blanchette-et-al-wit" and
+ "blanchette-et-al-2014-impl" and "panny-et-al-2014"}.
The central notion is that of a \emph{bounded natural functor} (BNF)---a
well-behaved type constructor for which nested (co)recursion is supported.
@@ -488,7 +489,7 @@
datatypes specified by their constructors.
The syntactic entity \synt{target} can be used to specify a local
-context (e.g., @{text "(in linorder)"} \cite{isabelle-isar-ref}),
+context (e.g., @{text "(in linorder)"} @{cite "isabelle-isar-ref"}),
and \synt{prop} denotes a HOL proposition.
The optional target is optionally followed by a combination of the following
@@ -527,7 +528,7 @@
\noindent
The syntactic entity \synt{name} denotes an identifier, \synt{mixfix} denotes
the usual parenthesized mixfix notation, and \synt{typefree} denotes fixed type
-variable (@{typ 'a}, @{typ 'b}, \ldots) \cite{isabelle-isar-ref}.
+variable (@{typ 'a}, @{typ 'b}, \ldots) @{cite "isabelle-isar-ref"}.
The optional names preceding the type variables allow to override the default
names of the set functions (@{text set\<^sub>1_t}, \ldots, @{text set\<^sub>m_t}). Type
@@ -561,7 +562,7 @@
\medskip
\noindent
-The syntactic entity \synt{type} denotes a HOL type \cite{isabelle-isar-ref}.
+The syntactic entity \synt{type} denotes a HOL type @{cite "isabelle-isar-ref"}.
In addition to the type of a constructor argument, it is possible to specify a
name for the corresponding selector to override the default name
@@ -596,7 +597,7 @@
ML {* Old_Datatype_Data.get_info @{theory} @{type_name even_nat} *}
text {*
-The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}.
+The syntactic entity \synt{name} denotes an identifier @{cite "isabelle-isar-ref"}.
The command can be useful because the old datatype package provides some
functionality that is not yet replicated in the new package.
@@ -1121,7 +1122,7 @@
command, which supports primitive recursion, or using the more general
\keyw{fun} and \keyw{function} commands. Here, the focus is on
@{command primrec}; the other two commands are described in a separate
-tutorial \cite{isabelle-function}.
+tutorial @{cite "isabelle-function"}.
%%% TODO: partial_function
*}
@@ -1473,7 +1474,7 @@
The syntactic entity \synt{target} can be used to specify a local context,
\synt{fixes} denotes a list of names with optional type signatures,
\synt{thmdecl} denotes an optional name for the formula that follows, and
-\synt{prop} denotes a HOL proposition \cite{isabelle-isar-ref}.
+\synt{prop} denotes a HOL proposition @{cite "isabelle-isar-ref"}.
The optional target is optionally followed by the following option:
@@ -1606,7 +1607,7 @@
flavors of corecursion. More examples can be found in the directory
\verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|. The
\emph{Archive of Formal Proofs} also includes some useful codatatypes, notably
-for lazy lists \cite{lochbihler-2010}.
+for lazy lists @{cite "lochbihler-2010"}.
*}
@@ -2408,7 +2409,7 @@
The syntactic entity \synt{target} can be used to specify a local context,
\synt{fixes} denotes a list of names with optional type signatures,
\synt{thmdecl} denotes an optional name for the formula that follows, and
-\synt{prop} denotes a HOL proposition \cite{isabelle-isar-ref}.
+\synt{prop} denotes a HOL proposition @{cite "isabelle-isar-ref"}.
The optional target is optionally followed by one or both of the following
options:
@@ -2468,7 +2469,7 @@
text {*
Bounded natural functors (BNFs) are a semantic criterion for where
(co)re\-cur\-sion may appear on the right-hand side of an equation
-\cite{traytel-et-al-2012,blanchette-et-al-wit}.
+@{cite "traytel-et-al-2012" and "blanchette-et-al-wit"}.
An $n$-ary BNF is a type constructor equipped with a map function
(functorial action), $n$ set functions (natural transformations),
@@ -2641,7 +2642,7 @@
The syntactic entity \synt{target} can be used to specify a local context,
\synt{type} denotes a HOL type, and \synt{term} denotes a HOL term
-\cite{isabelle-isar-ref}.
+@{cite "isabelle-isar-ref"}.
%%% TODO: elaborate on proof obligations
*}
@@ -2673,7 +2674,7 @@
The syntactic entity \synt{target} can be used to specify a local context,
\synt{name} denotes an identifier, \synt{typefree} denotes fixed type variable
(@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix} denotes the usual
-parenthesized mixfix notation \cite{isabelle-isar-ref}.
+parenthesized mixfix notation @{cite "isabelle-isar-ref"}.
Type arguments are live by default; they can be marked as dead by entering
@{text dead} in front of the type variable (e.g., @{text "(dead 'a)"})
@@ -2755,7 +2756,7 @@
The syntactic entity \synt{target} can be used to specify a local context,
\synt{name} denotes an identifier, \synt{prop} denotes a HOL proposition, and
-\synt{term} denotes a HOL term \cite{isabelle-isar-ref}.
+\synt{term} denotes a HOL term @{cite "isabelle-isar-ref"}.
The syntax resembles that of @{command datatype} and @{command codatatype}
definitions (Sections
--- a/src/Doc/Functions/Functions.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Functions/Functions.thy Tue Oct 07 22:35:11 2014 +0200
@@ -278,7 +278,7 @@
text {*
To see how the automatic termination proofs work, let's look at an
example where it fails\footnote{For a detailed discussion of the
- termination prover, see \cite{bulwahnKN07}}:
+ termination prover, see @{cite bulwahnKN07}}:
\end{isamarkuptext}
\cmd{fun} @{text "fails :: \"nat \<Rightarrow> nat list \<Rightarrow> nat\""}\\%
@@ -334,7 +334,7 @@
more powerful @{text size_change} method, which uses a variant of
the size-change principle, together with some other
techniques. While the details are discussed
- elsewhere\cite{krauss_phd},
+ elsewhere @{cite krauss_phd},
here are a few typical situations where
@{text lexicographic_order} has difficulties and @{text size_change}
may be worth a try:
--- a/src/Doc/Locales/Examples.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Locales/Examples.thy Tue Oct 07 22:35:11 2014 +0200
@@ -295,7 +295,7 @@
exception of the context elements \isakeyword{constrains} and
\isakeyword{defines}, which are provided for backward
compatibility. See the Isabelle/Isar Reference
- Manual~\cite{IsarRef} for full documentation. *}
+ Manual @{cite IsarRef} for full documentation. *}
section {* Import \label{sec:import} *}
@@ -763,7 +763,7 @@
The sublocale relation is transitive --- that is, propagation takes
effect along chains of sublocales. Even cycles in the sublocale relation are
supported, as long as these cycles do not lead to infinite chains.
- Details are discussed in the technical report \cite{Ballarin2006a}.
+ Details are discussed in the technical report @{cite Ballarin2006a}.
See also Section~\ref{sec:infinite-chains} of this tutorial. *}
end
--- a/src/Doc/Locales/Examples3.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Locales/Examples3.thy Tue Oct 07 22:35:11 2014 +0200
@@ -502,13 +502,13 @@
text {* More information on locales and their interpretation is
available. For the locale hierarchy of import and interpretation
- dependencies see~\cite{Ballarin2006a}; interpretations in theories
- and proofs are covered in~\cite{Ballarin2006b}. In the latter, I
+ dependencies see~@{cite Ballarin2006a}; interpretations in theories
+ and proofs are covered in~@{cite Ballarin2006b}. In the latter, I
show how interpretation in proofs enables to reason about families
of algebraic structures, which cannot be expressed with locales
directly.
- Haftmann and Wenzel~\cite{HaftmannWenzel2007} overcome a restriction
+ Haftmann and Wenzel~@{cite HaftmannWenzel2007} overcome a restriction
of axiomatic type classes through a combination with locale
interpretation. The result is a Haskell-style class system with a
facility to generate ML and Haskell code. Classes are sufficient for
@@ -520,14 +520,14 @@
The locales reimplementation for Isabelle 2009 provides, among other
improvements, a clean integration with Isabelle/Isar's local theory
mechanisms, which are described in another paper by Haftmann and
- Wenzel~\cite{HaftmannWenzel2009}.
+ Wenzel~@{cite HaftmannWenzel2009}.
- The original work of Kamm\"uller on locales~\cite{KammullerEtAl1999}
+ The original work of Kamm\"uller on locales~@{cite KammullerEtAl1999}
may be of interest from a historical perspective. My previous
- report on locales and locale expressions~\cite{Ballarin2004a}
+ report on locales and locale expressions~@{cite Ballarin2004a}
describes a simpler form of expressions than available now and is
outdated. The mathematical background on orders and lattices is
- taken from Jacobson's textbook on algebra~\cite[Chapter~8]{Jacobson1985}.
+ taken from Jacobson's textbook on algebra~@{cite \<open>Chapter~8\<close> Jacobson1985}.
The sources of this tutorial, which include all proofs, are
available with the Isabelle distribution at
--- a/src/Doc/Logics_ZF/ZF_Isar.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Logics_ZF/ZF_Isar.thy Tue Oct 07 22:35:11 2014 +0200
@@ -94,7 +94,7 @@
hints: @{syntax (ZF) "monos"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
\<close>}
- See \cite{isabelle-ZF} for further information on inductive
+ See @{cite "isabelle-ZF"} for further information on inductive
definitions in ZF, but note that this covers the old-style theory
format.
*}
--- a/src/Doc/Prog_Prove/Logic.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Prog_Prove/Logic.thy Tue Oct 07 22:35:11 2014 +0200
@@ -139,7 +139,7 @@
@{thm image_def}\index{$IMP042@@{term"f ` A"}} & is the image of a function over a set
\end{tabular}
\end{center}
-See \cite{Nipkow-Main} for the wealth of further predefined functions in theory
+See @{cite "Nipkow-Main"} for the wealth of further predefined functions in theory
@{theory Main}.
@@ -399,7 +399,7 @@
{\mbox{@{text"?P = ?Q"}}}
\]
These rules are part of the logical system of \concept{natural deduction}
-(e.g., \cite{HuthRyan}). Although we intentionally de-emphasize the basic rules
+(e.g., @{cite HuthRyan}). Although we intentionally de-emphasize the basic rules
of logic in favour of automatic proof methods that allow you to take bigger
steps, these rules are helpful in locating where and why automation fails.
When applied backwards, these rules decompose the goal:
@@ -486,7 +486,7 @@
%
%Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current
%theory. Search criteria include pattern matching on terms and on names.
-%For details see the Isabelle/Isar Reference Manual~\cite{IsarRef}.
+%For details see the Isabelle/Isar Reference Manual~@{cite IsarRef}.
%\bigskip
\begin{warn}
--- a/src/Doc/Prog_Prove/Types_and_funs.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Tue Oct 07 22:35:11 2014 +0200
@@ -148,7 +148,7 @@
is measured as the number of constructors (excluding 0-ary ones, e.g., @{text
Nil}). Lexicographic combinations are also recognized. In more complicated
situations, the user may have to prove termination by hand. For details
-see~\cite{Krauss}.
+see~@{cite Krauss}.
Functions defined with \isacom{fun} come with their own induction schema
that mirrors the recursion schema and is derived from the termination
--- a/src/Doc/Sugar/Sugar.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Sugar/Sugar.thy Tue Oct 07 22:35:11 2014 +0200
@@ -14,7 +14,7 @@
@{thm[display,mode=latex_sum] setsum_Suc_diff[no_vars]}
No typos, no omissions, no sweat.
If you have not experienced that joy, read Chapter 4, \emph{Presenting
-Theories}, \cite{LNCS2283} first.
+Theories}, @{cite LNCS2283} first.
If you have mastered the art of Isabelle's \emph{antiquotations},
i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
@@ -180,7 +180,7 @@
\subsection{Inference rules}
To print theorems as inference rules you need to include Didier
-R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
+R\'emy's \texttt{mathpartir} package~@{cite mathpartir}
for typesetting inference rules in your \LaTeX\ file.
Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
--- a/src/Doc/Tutorial/Advanced/WFrec.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Advanced/WFrec.thy Tue Oct 07 22:35:11 2014 +0200
@@ -29,7 +29,7 @@
left-hand side of an equation and $r$ the argument of some recursive call on
the corresponding right-hand side, induces a well-founded relation. For a
systematic account of termination proofs via well-founded relations see, for
-example, Baader and Nipkow~\cite{Baader-Nipkow}.
+example, Baader and Nipkow~@{cite "Baader-Nipkow"}.
Each \isacommand{recdef} definition should be accompanied (after the function's
name) by a well-founded relation on the function's argument type.
--- a/src/Doc/Tutorial/Advanced/simp2.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Advanced/simp2.thy Tue Oct 07 22:35:11 2014 +0200
@@ -123,7 +123,7 @@
rewrite rules. This is not quite true. For reasons of feasibility,
the simplifier expects the
left-hand side of each rule to be a so-called \emph{higher-order
-pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}.
+pattern}~@{cite "nipkow-patterns"}\indexbold{patterns!higher-order}.
This restricts where
unknowns may occur. Higher-order patterns are terms in $\beta$-normal
form. (This means there are no subterms of the form $(\lambda x. M)(N)$.)
--- a/src/Doc/Tutorial/CTL/Base.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/CTL/Base.thy Tue Oct 07 22:35:11 2014 +0200
@@ -7,7 +7,7 @@
Computation Tree Logic (CTL), a temporal logic.
Model checking is a popular technique for the verification of finite
state systems (implementations) with respect to temporal logic formulae
-(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic
+(specifications) @{cite "ClarkeGP-book" and "Huth-Ryan-book"}. Its foundations are set theoretic
and this section will explore them in HOL\@. This is done in two steps. First
we consider a simple modal logic called propositional dynamic
logic (PDL)\@. We then proceed to the temporal logic CTL, which is
--- a/src/Doc/Tutorial/CTL/CTL.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/CTL/CTL.thy Tue Oct 07 22:35:11 2014 +0200
@@ -361,7 +361,7 @@
%{text[display]"| EU formula formula E[_ U _]"}
%which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
\end{exercise}
-For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}.
+For more CTL exercises see, for example, Huth and Ryan @{cite "Huth-Ryan-book"}.
*}
(*<*)
@@ -439,7 +439,7 @@
our model checkers. It is clear that if all sets are finite, they can be
represented as lists and the usual set operations are easily
implemented. Only @{const lfp} requires a little thought. Fortunately, theory
-@{text While_Combinator} in the Library~\cite{HOL-Library} provides a
+@{text While_Combinator} in the Library~@{cite "HOL-Library"} provides a
theorem stating that in the case of finite sets and a monotone
function~@{term F}, the value of \mbox{@{term"lfp F"}} can be computed by
iterated application of @{term F} to~@{term"{}"} until a fixed point is
--- a/src/Doc/Tutorial/CTL/PDL.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/CTL/PDL.thy Tue Oct 07 22:35:11 2014 +0200
@@ -8,7 +8,7 @@
connectives @{text AX} and @{text EF}\@. Since formulae are essentially
syntax trees, they are naturally modelled as a datatype:%
\footnote{The customary definition of PDL
-\cite{HarelKT-DL} looks quite different from ours, but the two are easily
+@{cite "HarelKT-DL"} looks quite different from ours, but the two are easily
shown to be equivalent.}
*}
--- a/src/Doc/Tutorial/Datatype/Nested.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Datatype/Nested.thy Tue Oct 07 22:35:11 2014 +0200
@@ -150,7 +150,7 @@
instead. Simple uses of \isacommand{fun} are described in
\S\ref{sec:fun} below. Advanced applications, including functions
over nested datatypes like @{text term}, are discussed in a
-separate tutorial~\cite{isabelle-function}.
+separate tutorial~@{cite "isabelle-function"}.
Of course, you may also combine mutual and nested recursion of datatypes. For example,
constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
--- a/src/Doc/Tutorial/Documents/Documents.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Documents/Documents.thy Tue Oct 07 22:35:11 2014 +0200
@@ -11,7 +11,7 @@
for the parser and output templates for the pretty printer.
In full generality, parser and pretty printer configuration is a
- subtle affair~\cite{isabelle-isar-ref}. Your syntax specifications need
+ subtle affair~@{cite "isabelle-isar-ref"}. Your syntax specifications need
to interact properly with the existing setup of Isabelle/Pure and
Isabelle/HOL\@. To avoid creating ambiguities with existing
elements, it is particularly important to give new syntactic
@@ -107,7 +107,7 @@
\verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
A list of standard Isabelle symbols is given in
- \cite{isabelle-isar-ref}. You may introduce your own
+ @{cite "isabelle-isar-ref"}. You may introduce your own
interpretation of further symbols by configuring the appropriate
front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
@@ -153,7 +153,7 @@
be displayed after further input.
More flexible is to provide alternative syntax forms
- through the \bfindex{print mode} concept~\cite{isabelle-isar-ref}. By
+ through the \bfindex{print mode} concept~@{cite "isabelle-isar-ref"}. By
convention, the mode of ``$xsymbols$'' is enabled whenever
Proof~General's X-Symbol mode or {\LaTeX} output is active. Now
consider the following hybrid declaration of @{text xor}:
@@ -187,7 +187,7 @@
text {*
Prefix syntax annotations\index{prefix annotation} are another form
- of mixfixes \cite{isabelle-isar-ref}, without any template arguments or
+ of mixfixes @{cite "isabelle-isar-ref"}, without any template arguments or
priorities --- just some literal syntax. The following example
associates common symbols with the constructors of a datatype.
*}
@@ -262,7 +262,7 @@
Abbreviations are a simplified form of the general concept of
\emph{syntax translations}; even heavier transformations may be
-written in ML \cite{isabelle-isar-ref}.
+written in ML @{cite "isabelle-isar-ref"}.
*}
@@ -351,7 +351,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-sys"}.
For example, a new session \texttt{MySession} (with document
preparation) may be produced as follows:
@@ -412,7 +412,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-sys"}.
\medskip Any failure of the document preparation phase in an
Isabelle batch session leaves the generated sources in their target
@@ -526,7 +526,7 @@
theory or proof context (\bfindex{text blocks}).
\medskip Marginal comments are part of each command's concrete
- syntax \cite{isabelle-isar-ref}; the common form is ``\verb,--,~$text$''
+ syntax @{cite "isabelle-isar-ref"}; the common form is ``\verb,--,~$text$''
where $text$ is delimited by \verb,",@{text \<dots>}\verb,", or
\verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,}, as before. Multiple
marginal comments may be given at the same time. Here is a simple
@@ -612,7 +612,7 @@
same types as they have in the main goal statement.
\medskip Several further kinds of antiquotations and options are
- available \cite{isabelle-isar-ref}. Here are a few commonly used
+ available @{cite "isabelle-isar-ref"}. Here are a few commonly used
combinations:
\medskip
@@ -661,7 +661,7 @@
straightforward generalization of ASCII characters. While Isabelle
does not impose any interpretation of the infinite collection of
named symbols, {\LaTeX} documents use canonical glyphs for certain
- standard symbols \cite{isabelle-isar-ref}.
+ standard symbols @{cite "isabelle-isar-ref"}.
The {\LaTeX} code produced from Isabelle text follows a simple
scheme. You can tune the final appearance by redefining certain
@@ -751,7 +751,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-sys"} for further details, especially on
\texttt{isabelle build} and \texttt{isabelle document}.
Ignored material is specified by delimiting the original formal
--- a/src/Doc/Tutorial/Fun/fun0.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Fun/fun0.thy Tue Oct 07 22:35:11 2014 +0200
@@ -96,7 +96,7 @@
text{* The order of arguments has no influence on whether
\isacommand{fun} can prove termination of a function. For more details
-see elsewhere~\cite{bulwahnKN07}.
+see elsewhere~@{cite bulwahnKN07}.
\subsection{Simplification}
\label{sec:fun-simplification}
--- a/src/Doc/Tutorial/Inductive/AB.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Inductive/AB.thy Tue Oct 07 22:35:11 2014 +0200
@@ -17,7 +17,7 @@
B &\to& b S \mid a B B \nonumber
\end{eqnarray}
At the end we say a few words about the relationship between
-the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version.
+the original proof @{cite \<open>p.\ts81\<close> HopcroftUllman} and our formal version.
We start by fixing the alphabet, which consists only of @{term a}'s
and~@{term b}'s:
@@ -283,7 +283,7 @@
text{*
We conclude this section with a comparison of our proof with
Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
-\cite[p.\ts81]{HopcroftUllman}.
+@{cite \<open>p.\ts81\<close> HopcroftUllman}.
For a start, the textbook
grammar, for no good reason, excludes the empty word, thus complicating
matters just a little bit: they have 8 instead of our 7 productions.
--- a/src/Doc/Tutorial/Protocol/NS_Public.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Protocol/NS_Public.thy Tue Oct 07 22:35:11 2014 +0200
@@ -381,8 +381,8 @@
\medskip
Detailed information on this protocol verification technique can be found
-elsewhere~\cite{paulson-jcs}, including proofs of an Internet
-protocol~\cite{paulson-tls}. We must stress that the protocol discussed
+elsewhere~@{cite "paulson-jcs"}, including proofs of an Internet
+protocol~@{cite "paulson-tls"}. We must stress that the protocol discussed
in this chapter is trivial. There are only three messages; no keys are
exchanged; we merely have to prove that encrypted data remains secret.
Real world protocols are much longer and distribute many secrets to their
@@ -391,7 +391,7 @@
been used to encrypt other sensitive information, there may be cascading
losses. We may still be able to establish a bound on the losses and to
prove that other protocol runs function
-correctly~\cite{paulson-yahalom}. Proofs of real-world protocols follow
+correctly~@{cite "paulson-yahalom"}. Proofs of real-world protocols follow
the strategy illustrated above, but the subgoals can
be much bigger and there are more of them.
\index{protocols!security|)}
--- a/src/Doc/Tutorial/Types/Axioms.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Types/Axioms.thy Tue Oct 07 22:35:11 2014 +0200
@@ -8,7 +8,7 @@
\begin{warn}
Proofs in this section use structured \emph{Isar} proofs, which are not
-covered in this tutorial; but see \cite{Nipkow-TYPES02}.%
+covered in this tutorial; but see @{cite "Nipkow-TYPES02"}.%
\end{warn} *}
subsubsection {* Semigroups *}
--- a/src/Doc/Tutorial/Types/Records.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Types/Records.thy Tue Oct 07 22:35:11 2014 +0200
@@ -33,7 +33,7 @@
text {*
Record types are not primitive in Isabelle and have a delicate
- internal representation \cite{NaraschewskiW-TPHOLs98}, based on
+ internal representation @{cite "NaraschewskiW-TPHOLs98"}, based on
nested copies of the primitive product type. A \commdx{record}
declaration introduces a new record type scheme by specifying its
fields, which are packaged internally to hold up the perception of
--- a/src/Doc/Tutorial/Types/Typedefs.thy Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Types/Typedefs.thy Tue Oct 07 22:35:11 2014 +0200
@@ -216,7 +216,7 @@
example to demonstrate \isacommand{typedef} because its simplicity makes the
key concepts particularly easy to grasp. If you would like to see a
non-trivial example that cannot be defined more directly, we recommend the
-definition of \emph{finite multisets} in the Library~\cite{HOL-Library}.
+definition of \emph{finite multisets} in the Library~@{cite "HOL-Library"}.
Let us conclude by summarizing the above procedure for defining a new type.
Given some abstract axiomatic description $P$ of a type $ty$ in terms of a