author | wenzelm |

Tue Oct 07 23:12:08 2014 +0200 (2014-10-07) | |

changeset 58622 | aa99568f56de |

parent 58621 | 7a2c567061b3 |

child 58623 | 2db1df2c8467 |

more antiquotations;

1.1 --- a/src/HOL/Algebra/Group.thy Tue Oct 07 22:54:49 2014 +0200 1.2 +++ b/src/HOL/Algebra/Group.thy Tue Oct 07 23:12:08 2014 +0200 1.3 @@ -13,7 +13,7 @@ 1.4 subsection {* Definitions *} 1.5 1.6 text {* 1.7 - Definitions follow \cite{Jacobson:1985}. 1.8 + Definitions follow @{cite "Jacobson:1985"}. 1.9 *} 1.10 1.11 record 'a monoid = "'a partial_object" +

2.1 --- a/src/HOL/Algebra/Sylow.thy Tue Oct 07 22:54:49 2014 +0200 2.2 +++ b/src/HOL/Algebra/Sylow.thy Tue Oct 07 23:12:08 2014 +0200 2.3 @@ -7,7 +7,7 @@ 2.4 begin 2.5 2.6 text {* 2.7 - See also \cite{Kammueller-Paulson:1999}. 2.8 + See also @{cite "Kammueller-Paulson:1999"}. 2.9 *} 2.10 2.11 text{*The combinatorial argument is in theory Exponent*}

3.1 --- a/src/HOL/Algebra/UnivPoly.thy Tue Oct 07 22:54:49 2014 +0200 3.2 +++ b/src/HOL/Algebra/UnivPoly.thy Tue Oct 07 23:12:08 2014 +0200 3.3 @@ -18,7 +18,7 @@ 3.4 carrier set is a set of bounded functions from Nat to the 3.5 coefficient domain. Bounded means that these functions return zero 3.6 above a certain bound (the degree). There is a chapter on the 3.7 - formalisation of polynomials in the PhD thesis \cite{Ballarin:1999}, 3.8 + formalisation of polynomials in the PhD thesis @{cite "Ballarin:1999"}, 3.9 which was implemented with axiomatic type classes. This was later 3.10 ported to Locales. 3.11 *}

4.1 --- a/src/HOL/HOLCF/IMP/HoareEx.thy Tue Oct 07 22:54:49 2014 +0200 4.2 +++ b/src/HOL/HOLCF/IMP/HoareEx.thy Tue Oct 07 23:12:08 2014 +0200 4.3 @@ -9,7 +9,7 @@ 4.4 4.5 text {* 4.6 An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch 4.7 - \cite{MuellerNvOS99}. It demonstrates fixpoint reasoning by showing 4.8 + @{cite MuellerNvOS99}. It demonstrates fixpoint reasoning by showing 4.9 the correctness of the Hoare rule for while-loops. 4.10 *} 4.11

5.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Tue Oct 07 22:54:49 2014 +0200 5.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Tue Oct 07 23:12:08 2014 +0200 5.3 @@ -10,7 +10,7 @@ 5.4 5.5 text {* 5.6 We present the proof of two different versions of the Hahn-Banach 5.7 - Theorem, closely following \cite[\S36]{Heuser:1986}. 5.8 + Theorem, closely following @{cite \<open>\S36\<close> "Heuser:1986"}. 5.9 *} 5.10 5.11 subsection {* The Hahn-Banach Theorem for vector spaces *}

6.1 --- a/src/HOL/Imperative_HOL/Overview.thy Tue Oct 07 22:54:49 2014 +0200 6.2 +++ b/src/HOL/Imperative_HOL/Overview.thy Tue Oct 07 23:12:08 2014 +0200 6.3 @@ -24,8 +24,8 @@ 6.4 text {* 6.5 @{text "Imperative HOL"} is a leightweight framework for reasoning 6.6 about imperative data structures in @{text "Isabelle/HOL"} 6.7 - \cite{Nipkow-et-al:2002:tutorial}. Its basic ideas are described in 6.8 - \cite{Bulwahn-et-al:2008:imp_HOL}. However their concrete 6.9 + @{cite "Nipkow-et-al:2002:tutorial"}. Its basic ideas are described in 6.10 + @{cite "Bulwahn-et-al:2008:imp_HOL"}. However their concrete 6.11 realisation has changed since, due to both extensions and 6.12 refinements. Therefore this overview wants to present the framework 6.13 \qt{as it is} by now. It focusses on the user-view, less on matters

7.1 --- a/src/HOL/Lattice/CompleteLattice.thy Tue Oct 07 22:54:49 2014 +0200 7.2 +++ b/src/HOL/Lattice/CompleteLattice.thy Tue Oct 07 23:12:08 2014 +0200 7.3 @@ -110,7 +110,7 @@ 7.4 text {* 7.5 The Knaster-Tarski Theorem (in its simplest formulation) states that 7.6 any monotone function on a complete lattice has a least fixed-point 7.7 - (see \cite[pages 93--94]{Davey-Priestley:1990} for example). This 7.8 + (see @{cite \<open>pages 93--94\<close> "Davey-Priestley:1990"} for example). This 7.9 is a consequence of the basic boundary properties of the complete 7.10 lattice operations. 7.11 *}

8.1 --- a/src/HOL/Library/BigO.thy Tue Oct 07 22:54:49 2014 +0200 8.2 +++ b/src/HOL/Library/BigO.thy Tue Oct 07 23:12:08 2014 +0200 8.3 @@ -12,7 +12,7 @@ 8.4 This library is designed to support asymptotic ``big O'' calculations, 8.5 i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g + 8.6 O(h)$. An earlier version of this library is described in detail in 8.7 -\cite{Avigad-Donnelly}. 8.8 +@{cite "Avigad-Donnelly"}. 8.9 8.10 The main changes in this version are as follows: 8.11 \begin{itemize}

9.1 --- a/src/HOL/Library/Ramsey.thy Tue Oct 07 22:54:49 2014 +0200 9.2 +++ b/src/HOL/Library/Ramsey.thy Tue Oct 07 23:12:08 2014 +0200 9.3 @@ -338,7 +338,7 @@ 9.4 9.5 text {* 9.6 An application of Ramsey's theorem to program termination. See 9.7 - \cite{Podelski-Rybalchenko}. 9.8 + @{cite "Podelski-Rybalchenko"}. 9.9 *} 9.10 9.11 definition disj_wf :: "('a * 'a)set => bool"

10.1 --- a/src/HOL/Proofs/Extraction/Euclid.thy Tue Oct 07 22:54:49 2014 +0200 10.2 +++ b/src/HOL/Proofs/Extraction/Euclid.thy Tue Oct 07 23:12:08 2014 +0200 10.3 @@ -15,7 +15,7 @@ 10.4 10.5 text {* 10.6 A constructive version of the proof of Euclid's theorem by 10.7 -Markus Wenzel and Freek Wiedijk \cite{Wenzel-Wiedijk-JAR2002}. 10.8 +Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}. 10.9 *} 10.10 10.11 lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"

11.1 --- a/src/HOL/Proofs/Extraction/Higman.thy Tue Oct 07 22:54:49 2014 +0200 11.2 +++ b/src/HOL/Proofs/Extraction/Higman.thy Tue Oct 07 23:12:08 2014 +0200 11.3 @@ -11,7 +11,7 @@ 11.4 11.5 text {* 11.6 Formalization by Stefan Berghofer and Monika Seisenberger, 11.7 - based on Coquand and Fridlender \cite{Coquand93}. 11.8 + based on Coquand and Fridlender @{cite Coquand93}. 11.9 *} 11.10 11.11 datatype letter = A | B

12.1 --- a/src/HOL/Proofs/Extraction/Pigeonhole.thy Tue Oct 07 22:54:49 2014 +0200 12.2 +++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy Tue Oct 07 23:12:08 2014 +0200 12.3 @@ -12,7 +12,7 @@ 12.4 We formalize two proofs of the pigeonhole principle, which lead 12.5 to extracted programs of quite different complexity. The original 12.6 formalization of these proofs in {\sc Nuprl} is due to 12.7 -Aleksey Nogin \cite{Nogin-ENTCS-2000}. 12.8 +Aleksey Nogin @{cite "Nogin-ENTCS-2000"}. 12.9 12.10 This proof yields a polynomial program. 12.11 *}

13.1 --- a/src/HOL/Proofs/Extraction/Warshall.thy Tue Oct 07 22:54:49 2014 +0200 13.2 +++ b/src/HOL/Proofs/Extraction/Warshall.thy Tue Oct 07 23:12:08 2014 +0200 13.3 @@ -10,7 +10,7 @@ 13.4 13.5 text {* 13.6 Derivation of Warshall's algorithm using program extraction, 13.7 - based on Berger, Schwichtenberg and Seisenberger \cite{Berger-JAR-2001}. 13.8 + based on Berger, Schwichtenberg and Seisenberger @{cite "Berger-JAR-2001"}. 13.9 *} 13.10 13.11 datatype b = T | F

14.1 --- a/src/HOL/Proofs/Lambda/Eta.thy Tue Oct 07 22:54:49 2014 +0200 14.2 +++ b/src/HOL/Proofs/Lambda/Eta.thy Tue Oct 07 23:12:08 2014 +0200 14.3 @@ -234,7 +234,7 @@ 14.4 14.5 text {* 14.6 Based on a paper proof due to Andreas Abel. 14.7 - Unlike the proof by Masako Takahashi \cite{Takahashi-IandC}, it does not 14.8 + Unlike the proof by Masako Takahashi @{cite "Takahashi-IandC"}, it does not 14.9 use parallel eta reduction, which only seems to complicate matters unnecessarily. 14.10 *} 14.11

15.1 --- a/src/HOL/Proofs/Lambda/Standardization.thy Tue Oct 07 22:54:49 2014 +0200 15.2 +++ b/src/HOL/Proofs/Lambda/Standardization.thy Tue Oct 07 23:12:08 2014 +0200 15.3 @@ -10,8 +10,8 @@ 15.4 begin 15.5 15.6 text {* 15.7 -Based on lecture notes by Ralph Matthes \cite{Matthes-ESSLLI2000}, 15.8 -original proof idea due to Ralph Loader \cite{Loader1998}. 15.9 +Based on lecture notes by Ralph Matthes @{cite "Matthes-ESSLLI2000"}, 15.10 +original proof idea due to Ralph Loader @{cite Loader1998}. 15.11 *} 15.12 15.13

16.1 --- a/src/HOL/Proofs/Lambda/StrongNorm.thy Tue Oct 07 22:54:49 2014 +0200 16.2 +++ b/src/HOL/Proofs/Lambda/StrongNorm.thy Tue Oct 07 23:12:08 2014 +0200 16.3 @@ -9,7 +9,7 @@ 16.4 16.5 text {* 16.6 Formalization by Stefan Berghofer. Partly based on a paper proof by 16.7 -Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}. 16.8 +Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}. 16.9 *} 16.10 16.11

17.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Oct 07 22:54:49 2014 +0200 17.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Oct 07 23:12:08 2014 +0200 17.3 @@ -12,7 +12,7 @@ 17.4 17.5 text {* 17.6 Formalization by Stefan Berghofer. Partly based on a paper proof by 17.7 -Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}. 17.8 +Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}. 17.9 *} 17.10 17.11

18.1 --- a/src/HOL/SPARK/Manual/Example_Verification.thy Tue Oct 07 22:54:49 2014 +0200 18.2 +++ b/src/HOL/SPARK/Manual/Example_Verification.thy Tue Oct 07 23:12:08 2014 +0200 18.3 @@ -23,7 +23,7 @@ 18.4 We will now explain the usage of the \SPARK{} verification environment by proving 18.5 the correctness of an example program. As an example, we use a program for computing 18.6 the \emph{greatest common divisor} of two natural numbers shown in \figref{fig:gcd-prog}, 18.7 -which has been taken from the book about \SPARK{} by Barnes \cite[\S 11.6]{Barnes}. 18.8 +which has been taken from the book about \SPARK{} by Barnes @{cite \<open>\S 11.6\<close> Barnes}. 18.9 *} 18.10 18.11 section {* Importing \SPARK{} VCs into Isabelle *} 18.12 @@ -228,7 +228,7 @@ 18.13 are trivially proved to be non-negative. Since we are working with non-negative 18.14 numbers, we can also just use \SPARK{}'s \textbf{mod} operator instead of 18.15 \textbf{rem}, which spares us an application of theorems @{text zmod_zdiv_equality'} 18.16 -and @{text sdiv_pos_pos}. Finally, as noted by Barnes \cite[\S 11.5]{Barnes}, 18.17 +and @{text sdiv_pos_pos}. Finally, as noted by Barnes @{cite \<open>\S 11.5\<close> Barnes}, 18.18 we can simplify matters by placing the \textbf{assert} statement between 18.19 \textbf{while} and \textbf{loop} rather than directly after the \textbf{loop}. 18.20 In the former case, the loop invariant has to be proved only once, whereas in

19.1 --- a/src/HOL/SPARK/Manual/VC_Principles.thy Tue Oct 07 22:54:49 2014 +0200 19.2 +++ b/src/HOL/SPARK/Manual/VC_Principles.thy Tue Oct 07 23:12:08 2014 +0200 19.3 @@ -76,7 +76,7 @@ 19.4 \caption{Control flow graph for procedure \texttt{Proc2}} 19.5 \label{fig:proc2-graph} 19.6 \end{figure} 19.7 -As explained by Barnes \cite[\S 11.5]{Barnes}, the \SPARK{} Examiner unfolds the loop 19.8 +As explained by Barnes @{cite \<open>\S 11.5\<close> Barnes}, the \SPARK{} Examiner unfolds the loop 19.9 \begin{lstlisting} 19.10 for I in T range L .. U loop 19.11 --# assert P (I);

20.1 --- a/src/HOL/ex/CTL.thy Tue Oct 07 22:54:49 2014 +0200 20.2 +++ b/src/HOL/ex/CTL.thy Tue Oct 07 23:12:08 2014 +0200 20.3 @@ -10,7 +10,7 @@ 20.4 20.5 text {* 20.6 We formalize basic concepts of Computational Tree Logic (CTL) 20.7 - \cite{McMillan-PhDThesis,McMillan-LectureNotes} within the 20.8 + @{cite "McMillan-PhDThesis" and "McMillan-LectureNotes"} within the 20.9 simply-typed set theory of HOL. 20.10 20.11 By using the common technique of ``shallow embedding'', a CTL 20.12 @@ -55,7 +55,7 @@ 20.13 such that for all states @{term s'} on the path, @{term p} holds in 20.14 @{term s'}. It is easy to see that @{text "\<EF> p"} and @{text 20.15 "\<EG> p"} may be expressed using least and greatest fixed points 20.16 - \cite{McMillan-PhDThesis}. 20.17 + @{cite "McMillan-PhDThesis"}. 20.18 *} 20.19 20.20 definition

21.1 --- a/src/HOL/ex/Higher_Order_Logic.thy Tue Oct 07 22:54:49 2014 +0200 21.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy Tue Oct 07 23:12:08 2014 +0200 21.3 @@ -10,7 +10,7 @@ 21.4 The following theory development demonstrates Higher-Order Logic 21.5 itself, represented directly within the Pure framework of Isabelle. 21.6 The ``HOL'' logic given here is essentially that of Gordon 21.7 - \cite{Gordon:1985:HOL}, although we prefer to present basic concepts 21.8 + @{cite "Gordon:1985:HOL"}, although we prefer to present basic concepts 21.9 in a slightly more conventional manner oriented towards plain 21.10 Natural Deduction. 21.11 *}