more antiquotations;
authorwenzelm
Tue Oct 07 23:12:08 2014 +0200 (2014-10-07)
changeset 58622aa99568f56de
parent 58621 7a2c567061b3
child 58623 2db1df2c8467
more antiquotations;
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/HOLCF/IMP/HoareEx.thy
src/HOL/Hahn_Banach/Hahn_Banach.thy
src/HOL/Imperative_HOL/Overview.thy
src/HOL/Lattice/CompleteLattice.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Ramsey.thy
src/HOL/Proofs/Extraction/Euclid.thy
src/HOL/Proofs/Extraction/Higman.thy
src/HOL/Proofs/Extraction/Pigeonhole.thy
src/HOL/Proofs/Extraction/Warshall.thy
src/HOL/Proofs/Lambda/Eta.thy
src/HOL/Proofs/Lambda/Standardization.thy
src/HOL/Proofs/Lambda/StrongNorm.thy
src/HOL/Proofs/Lambda/WeakNorm.thy
src/HOL/SPARK/Manual/Example_Verification.thy
src/HOL/SPARK/Manual/VC_Principles.thy
src/HOL/ex/CTL.thy
src/HOL/ex/Higher_Order_Logic.thy
     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  *}