--- 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
--- 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
--- 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. *}
--- 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.