# HG changeset patch
# User wenzelm
# Date 1412541973 -7200
# Node ID 3876a1a9ee42b12416aed43d373a53e035718504
# Parent  66fed99e874fb7f3af9f5f40c54c0d0075a077ca
prefer @{cite} antiquotation;

diff -r 66fed99e874f -r 3876a1a9ee42 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Sun Oct 05 22:24:07 2014 +0200
+++ b/src/Doc/System/Basics.thy	Sun Oct 05 22:46:13 2014 +0200
@@ -6,10 +6,10 @@
 
 text {* This manual describes Isabelle together with related tools and
   user interfaces as seen from a system oriented view.  See also the
-  \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
+  \emph{Isabelle/Isar Reference Manual} @{cite "isabelle-isar-ref"} for
   the actual Isabelle input language and related concepts, and
   \emph{The Isabelle/Isar Implementation
-  Manual}~\cite{isabelle-implementation} for the main concepts of the
+  Manual} @{cite "isabelle-implementation"} for the main concepts of the
   underlying implementation in Isabelle/ML.
 
   \medskip The Isabelle system environment provides the following
diff -r 66fed99e874f -r 3876a1a9ee42 src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Sun Oct 05 22:24:07 2014 +0200
+++ b/src/Doc/System/Presentation.thy	Sun Oct 05 22:46:13 2014 +0200
@@ -244,7 +244,7 @@
   "isabellesym.sty"} should be included as well.  This package
   contains a standard set of {\LaTeX} macro definitions @{verbatim
   "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim
-  "<"}@{text foo}@{verbatim ">"}, see \cite{isabelle-implementation} for a
+  "<"}@{text foo}@{verbatim ">"}, see @{cite "isabelle-implementation"} for a
   complete list of predefined Isabelle symbols.  Users may invent
   further symbols as well, just by providing {\LaTeX} macros in a
   similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of
diff -r 66fed99e874f -r 3876a1a9ee42 src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Sun Oct 05 22:24:07 2014 +0200
+++ b/src/Doc/System/Scala.thy	Sun Oct 05 22:46:13 2014 +0200
@@ -8,7 +8,7 @@
 environments for Isabelle tool implementations.  There are some basic
 command-line tools to work with the underlying Java Virtual Machine,
 the Scala toplevel and compiler.  Note that Isabelle/jEdit
-\cite{isabelle-jedit} provides a Scala Console for interactive
+@{cite "isabelle-jedit"} provides a Scala Console for interactive
 experimentation within the running application. *}
 
 
@@ -66,7 +66,7 @@
   add-on components can register themselves in a modular manner, see
   also \secref{sec:components}.
 
-  Note that jEdit \cite{isabelle-jedit} has its own mechanisms for
+  Note that jEdit @{cite "isabelle-jedit"} has its own mechanisms for
   adding plugin components, which needs special attention since
   it overrides the standard Java class loader.  *}
 
diff -r 66fed99e874f -r 3876a1a9ee42 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sun Oct 05 22:24:07 2014 +0200
+++ b/src/Doc/System/Sessions.thy	Sun Oct 05 22:46:13 2014 +0200
@@ -36,7 +36,7 @@
 
   The ROOT file format follows the lexical conventions of the
   \emph{outer syntax} of Isabelle/Isar, see also
-  \cite{isabelle-isar-ref}.  This defines common forms like
+  @{cite "isabelle-isar-ref"}.  This defines common forms like
   identifiers, names, quoted strings, verbatim text, nested comments
   etc.  The grammar for @{syntax session_chapter} and @{syntax
   session_entry} is given as syntax diagram below; each ROOT file may
@@ -44,7 +44,7 @@
   organize browser info (\secref{sec:info}), but have no formal
   meaning.  The default chapter is ``@{text "Unsorted"}''.
 
-  Isabelle/jEdit \cite{isabelle-jedit} includes a simple editing
+  Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing
   mode @{verbatim "isabelle-root"} for session ROOT files, which is
   enabled by default for any file of that name.
 
@@ -161,7 +161,7 @@
 section {* System build options \label{sec:system-options} *}
 
 text {* See @{file "~~/etc/options"} for the main defaults provided by
-  the Isabelle distribution.  Isabelle/jEdit \cite{isabelle-jedit}
+  the Isabelle distribution.  Isabelle/jEdit @{cite "isabelle-jedit"}
   includes a simple editing mode @{verbatim "isabelle-options"} for
   this file-format.