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