# HG changeset patch
# User wenzelm
# Date 1412714111 -7200
# Node ID 7435b6a3f72e789691ce80efe11e09735734f0c6
# Parent  4b41df5fef811e43a74f4286c4188fdcc52bc0bf
more antiquotations;

diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Classes/Classes.thy
--- 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:
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Codegen/Evaluation.thy
--- 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.
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Codegen/Further.thy
--- 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.
 *}
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Codegen/Inductive_Predicate.thy
--- 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:
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Codegen/Introduction.thy
--- 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}
 
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Codegen/Refinement.thy
--- 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
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Datatypes/Datatypes.thy
--- 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
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Functions/Functions.thy
--- 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:
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Locales/Examples.thy
--- 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
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Locales/Examples3.thy
--- 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
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Logics_ZF/ZF_Isar.thy
--- 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.
 *}
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Prog_Prove/Logic.thy
--- 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}
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Prog_Prove/Types_and_funs.thy
--- 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
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Sugar/Sugar.thy
--- 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
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/Advanced/WFrec.thy
--- 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.  
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/Advanced/simp2.thy
--- 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)$.)  
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/CTL/Base.thy
--- 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
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/CTL/CTL.thy
--- 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
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/CTL/PDL.thy
--- 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.}
 *}
 
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/Datatype/Nested.thy
--- 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
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/Documents/Documents.thy
--- 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
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/Fun/fun0.thy
--- 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}
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/Inductive/AB.thy
--- 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.
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/Protocol/NS_Public.thy
--- 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|)}
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/Types/Axioms.thy
--- 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 *}
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/Types/Records.thy
--- 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
diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/Types/Typedefs.thy
--- 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