--- 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" +
--- 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*}
--- 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.
*}
--- 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.
*}
--- 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 *}
--- 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
--- 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.
*}
--- 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}
--- 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"
--- 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"
--- 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
--- 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.
*}
--- 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
--- 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.
*}
--- 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}.
*}
--- 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"}.
*}
--- 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"}.
*}
--- 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
--- 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);
--- 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
--- 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.
*}