# HG changeset patch
# User wenzelm
# Date 1412716328 -7200
# Node ID aa99568f56de1aeb346ce8813fd81ca2472f1718
# Parent  7a2c567061b389bafe662ab3f6d22b978b162640
more antiquotations;

diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Algebra/Group.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -13,7 +13,7 @@
 subsection {* Definitions *}
 
 text {*
-  Definitions follow \cite{Jacobson:1985}.
+  Definitions follow @{cite "Jacobson:1985"}.
 *}
 
 record 'a monoid =  "'a partial_object" +
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -7,7 +7,7 @@
 begin
 
 text {*
-  See also \cite{Kammueller-Paulson:1999}.
+  See also @{cite "Kammueller-Paulson:1999"}.
 *}
 
 text{*The combinatorial argument is in theory Exponent*}
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -18,7 +18,7 @@
   carrier set is a set of bounded functions from Nat to the
   coefficient domain.  Bounded means that these functions return zero
   above a certain bound (the degree).  There is a chapter on the
-  formalisation of polynomials in the PhD thesis \cite{Ballarin:1999},
+  formalisation of polynomials in the PhD thesis @{cite "Ballarin:1999"},
   which was implemented with axiomatic type classes.  This was later
   ported to Locales.
 *}
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/HOLCF/IMP/HoareEx.thy
--- a/src/HOL/HOLCF/IMP/HoareEx.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -9,7 +9,7 @@
 
 text {*
   An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch
-  \cite{MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
+  @{cite MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
   the correctness of the Hoare rule for while-loops.
 *}
 
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -10,7 +10,7 @@
 
 text {*
   We present the proof of two different versions of the Hahn-Banach
-  Theorem, closely following \cite[\S36]{Heuser:1986}.
+  Theorem, closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
 *}
 
 subsection {* The Hahn-Banach Theorem for vector spaces *}
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Imperative_HOL/Overview.thy
--- a/src/HOL/Imperative_HOL/Overview.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -24,8 +24,8 @@
 text {*
   @{text "Imperative HOL"} is a leightweight framework for reasoning
   about imperative data structures in @{text "Isabelle/HOL"}
-  \cite{Nipkow-et-al:2002:tutorial}.  Its basic ideas are described in
-  \cite{Bulwahn-et-al:2008:imp_HOL}.  However their concrete
+  @{cite "Nipkow-et-al:2002:tutorial"}.  Its basic ideas are described in
+  @{cite "Bulwahn-et-al:2008:imp_HOL"}.  However their concrete
   realisation has changed since, due to both extensions and
   refinements.  Therefore this overview wants to present the framework
   \qt{as it is} by now.  It focusses on the user-view, less on matters
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Lattice/CompleteLattice.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -110,7 +110,7 @@
 text {*
   The Knaster-Tarski Theorem (in its simplest formulation) states that
   any monotone function on a complete lattice has a least fixed-point
-  (see \cite[pages 93--94]{Davey-Priestley:1990} for example).  This
+  (see @{cite \<open>pages 93--94\<close> "Davey-Priestley:1990"} for example).  This
   is a consequence of the basic boundary properties of the complete
   lattice operations.
 *}
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Library/BigO.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -12,7 +12,7 @@
 This library is designed to support asymptotic ``big O'' calculations,
 i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g +
 O(h)$.  An earlier version of this library is described in detail in
-\cite{Avigad-Donnelly}.
+@{cite "Avigad-Donnelly"}.
 
 The main changes in this version are as follows:
 \begin{itemize}
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Library/Ramsey.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -338,7 +338,7 @@
 
 text {*
   An application of Ramsey's theorem to program termination. See
-  \cite{Podelski-Rybalchenko}.
+  @{cite "Podelski-Rybalchenko"}.
 *}
 
 definition disj_wf :: "('a * 'a)set => bool"
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Proofs/Extraction/Euclid.thy
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -15,7 +15,7 @@
 
 text {*
 A constructive version of the proof of Euclid's theorem by
-Markus Wenzel and Freek Wiedijk \cite{Wenzel-Wiedijk-JAR2002}.
+Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}.
 *}
 
 lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Proofs/Extraction/Higman.thy
--- a/src/HOL/Proofs/Extraction/Higman.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Proofs/Extraction/Higman.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -11,7 +11,7 @@
 
 text {*
   Formalization by Stefan Berghofer and Monika Seisenberger,
-  based on Coquand and Fridlender \cite{Coquand93}.
+  based on Coquand and Fridlender @{cite Coquand93}.
 *}
 
 datatype letter = A | B
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Proofs/Extraction/Pigeonhole.thy
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -12,7 +12,7 @@
 We formalize two proofs of the pigeonhole principle, which lead
 to extracted programs of quite different complexity. The original
 formalization of these proofs in {\sc Nuprl} is due to
-Aleksey Nogin \cite{Nogin-ENTCS-2000}.
+Aleksey Nogin @{cite "Nogin-ENTCS-2000"}.
 
 This proof yields a polynomial program.
 *}
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Proofs/Extraction/Warshall.thy
--- a/src/HOL/Proofs/Extraction/Warshall.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Proofs/Extraction/Warshall.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -10,7 +10,7 @@
 
 text {*
   Derivation of Warshall's algorithm using program extraction,
-  based on Berger, Schwichtenberg and Seisenberger \cite{Berger-JAR-2001}.
+  based on Berger, Schwichtenberg and Seisenberger @{cite "Berger-JAR-2001"}.
 *}
 
 datatype b = T | F
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Proofs/Lambda/Eta.thy
--- a/src/HOL/Proofs/Lambda/Eta.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Proofs/Lambda/Eta.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -234,7 +234,7 @@
 
 text {*
   Based on a paper proof due to Andreas Abel.
-  Unlike the proof by Masako Takahashi \cite{Takahashi-IandC}, it does not
+  Unlike the proof by Masako Takahashi @{cite "Takahashi-IandC"}, it does not
   use parallel eta reduction, which only seems to complicate matters unnecessarily.
 *}
 
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Proofs/Lambda/Standardization.thy
--- a/src/HOL/Proofs/Lambda/Standardization.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Proofs/Lambda/Standardization.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -10,8 +10,8 @@
 begin
 
 text {*
-Based on lecture notes by Ralph Matthes \cite{Matthes-ESSLLI2000},
-original proof idea due to Ralph Loader \cite{Loader1998}.
+Based on lecture notes by Ralph Matthes @{cite "Matthes-ESSLLI2000"},
+original proof idea due to Ralph Loader @{cite Loader1998}.
 *}
 
 
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Proofs/Lambda/StrongNorm.thy
--- a/src/HOL/Proofs/Lambda/StrongNorm.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Proofs/Lambda/StrongNorm.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -9,7 +9,7 @@
 
 text {*
 Formalization by Stefan Berghofer. Partly based on a paper proof by
-Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}.
+Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
 *}
 
 
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -12,7 +12,7 @@
 
 text {*
 Formalization by Stefan Berghofer. Partly based on a paper proof by
-Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}.
+Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
 *}
 
 
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/SPARK/Manual/Example_Verification.thy
--- a/src/HOL/SPARK/Manual/Example_Verification.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/SPARK/Manual/Example_Verification.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -23,7 +23,7 @@
 We will now explain the usage of the \SPARK{} verification environment by proving
 the correctness of an example program. As an example, we use a program for computing
 the \emph{greatest common divisor} of two natural numbers shown in \figref{fig:gcd-prog},
-which has been taken from the book about \SPARK{} by Barnes \cite[\S 11.6]{Barnes}.
+which has been taken from the book about \SPARK{} by Barnes @{cite \<open>\S 11.6\<close> Barnes}.
 *}
 
 section {* Importing \SPARK{} VCs into Isabelle *}
@@ -228,7 +228,7 @@
 are trivially proved to be non-negative. Since we are working with non-negative
 numbers, we can also just use \SPARK{}'s \textbf{mod} operator instead of
 \textbf{rem}, which spares us an application of theorems @{text zmod_zdiv_equality'}
-and @{text sdiv_pos_pos}. Finally, as noted by Barnes \cite[\S 11.5]{Barnes},
+and @{text sdiv_pos_pos}. Finally, as noted by Barnes @{cite \<open>\S 11.5\<close> Barnes},
 we can simplify matters by placing the \textbf{assert} statement between
 \textbf{while} and \textbf{loop} rather than directly after the \textbf{loop}.
 In the former case, the loop invariant has to be proved only once, whereas in
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/SPARK/Manual/VC_Principles.thy
--- a/src/HOL/SPARK/Manual/VC_Principles.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/SPARK/Manual/VC_Principles.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -76,7 +76,7 @@
 \caption{Control flow graph for procedure \texttt{Proc2}}
 \label{fig:proc2-graph}
 \end{figure}
-As explained by Barnes \cite[\S 11.5]{Barnes}, the \SPARK{} Examiner unfolds the loop
+As explained by Barnes @{cite \<open>\S 11.5\<close> Barnes}, the \SPARK{} Examiner unfolds the loop
 \begin{lstlisting}
 for I in T range L .. U loop
   --# assert P (I);
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/ex/CTL.thy
--- a/src/HOL/ex/CTL.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/ex/CTL.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -10,7 +10,7 @@
 
 text {*
   We formalize basic concepts of Computational Tree Logic (CTL)
-  \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the
+  @{cite "McMillan-PhDThesis" and "McMillan-LectureNotes"} within the
   simply-typed set theory of HOL.
 
   By using the common technique of ``shallow embedding'', a CTL
@@ -55,7 +55,7 @@
   such that for all states @{term s'} on the path, @{term p} holds in
   @{term s'}.  It is easy to see that @{text "\<EF> p"} and @{text
   "\<EG> p"} may be expressed using least and greatest fixed points
-  \cite{McMillan-PhDThesis}.
+  @{cite "McMillan-PhDThesis"}.
 *}
 
 definition
diff -r 7a2c567061b3 -r aa99568f56de src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -10,7 +10,7 @@
   The following theory development demonstrates Higher-Order Logic
   itself, represented directly within the Pure framework of Isabelle.
   The ``HOL'' logic given here is essentially that of Gordon
-  \cite{Gordon:1985:HOL}, although we prefer to present basic concepts
+  @{cite "Gordon:1985:HOL"}, although we prefer to present basic concepts
   in a slightly more conventional manner oriented towards plain
   Natural Deduction.
 *}