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