diff -r 423202f05a43 -r 7975676c08c0 src/Doc/Implementation/Logic.thy
--- 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: