more bibtex entries;
authorwenzelm
Tue Oct 07 23:29:43 2014 +0200 (2014-10-07)
changeset 586232db1df2c8467
parent 58622 aa99568f56de
child 58624 75b9b64ccb58
more bibtex entries;
more antiquotations;
src/HOL/BNF_Cardinal_Order_Relation.thy
src/HOL/GCD.thy
src/HOL/Induct/Comb.thy
src/HOL/Main.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Old_Number_Theory/Legacy_GCD.thy
src/HOL/Old_Number_Theory/document/root.bib
src/HOL/ROOT
src/HOL/Wellfounded.thy
src/HOL/document/root.bib
src/ZF/Induct/Acc.thy
src/ZF/Induct/Comb.thy
src/ZF/Induct/ListN.thy
src/ZF/Induct/Primrec.thy
src/ZF/Induct/document/root.bib
src/ZF/ROOT
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Oct 07 23:12:08 2014 +0200
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Oct 07 23:29:43 2014 +0200
     1.3 @@ -826,7 +826,7 @@
     1.4  theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
     1.5  does not increase cardinality -- the proof of this fact adapts a standard
     1.6  set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
     1.7 -at page 47 in \cite{card-book}. Then everything else follows fairly easily. *}
     1.8 +at page 47 in @{cite "card-book"}. Then everything else follows fairly easily. *}
     1.9  
    1.10  lemma infinite_iff_card_of_nat:
    1.11  "\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
     2.1 --- a/src/HOL/GCD.thy	Tue Oct 07 23:12:08 2014 +0200
     2.2 +++ b/src/HOL/GCD.thy	Tue Oct 07 23:29:43 2014 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  This file combines and revises a number of prior developments.
     2.5  
     2.6  The original theories "GCD" and "Primes" were by Christophe Tabacznyj
     2.7 -and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
     2.8 +and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
     2.9  gcd, lcm, and prime for the natural numbers.
    2.10  
    2.11  The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    2.12 @@ -364,7 +364,7 @@
    2.13  *}
    2.14  
    2.15  lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
    2.16 -    -- {* \cite[page 27]{davenport92} *}
    2.17 +    -- {* @{cite \<open>page 27\<close> davenport92} *}
    2.18    apply (induct m n rule: gcd_nat_induct)
    2.19    apply simp
    2.20    apply (case_tac "k = 0")
     3.1 --- a/src/HOL/Induct/Comb.thy	Tue Oct 07 23:12:08 2014 +0200
     3.2 +++ b/src/HOL/Induct/Comb.thy	Tue Oct 07 23:29:43 2014 +0200
     3.3 @@ -10,7 +10,7 @@
     3.4  text {*
     3.5    Curiously, combinators do not include free variables.
     3.6  
     3.7 -  Example taken from \cite{camilleri-melham}.
     3.8 +  Example taken from @{cite camilleri92}.
     3.9  
    3.10  HOL system proofs may be found in the HOL distribution at
    3.11     .../contrib/rule-induction/cl.ml
     4.1 --- a/src/HOL/Main.thy	Tue Oct 07 23:12:08 2014 +0200
     4.2 +++ b/src/HOL/Main.thy	Tue Oct 07 23:29:43 2014 +0200
     4.3 @@ -10,7 +10,7 @@
     4.4    complex numbers etc.
     4.5  *}
     4.6  
     4.7 -text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
     4.8 +text {* See further @{cite "Nipkow-et-al:2002:tutorial"} *}
     4.9  
    4.10  no_notation
    4.11    bot ("\<bottom>") and
     5.1 --- a/src/HOL/Number_Theory/Cong.thy	Tue Oct 07 23:12:08 2014 +0200
     5.2 +++ b/src/HOL/Number_Theory/Cong.thy	Tue Oct 07 23:29:43 2014 +0200
     5.3 @@ -8,7 +8,7 @@
     5.4  This file combines and revises a number of prior developments.
     5.5  
     5.6  The original theories "GCD" and "Primes" were by Christophe Tabacznyj
     5.7 -and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
     5.8 +and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
     5.9  gcd, lcm, and prime for the natural numbers.
    5.10  
    5.11  The original theory "IntPrimes" was by Thomas M. Rasmussen, and
     6.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Oct 07 23:12:08 2014 +0200
     6.2 +++ b/src/HOL/Number_Theory/Primes.thy	Tue Oct 07 23:29:43 2014 +0200
     6.3 @@ -8,7 +8,7 @@
     6.4  This file combines and revises a number of prior developments.
     6.5  
     6.6  The original theories "GCD" and "Primes" were by Christophe Tabacznyj
     6.7 -and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
     6.8 +and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
     6.9  gcd, lcm, and prime for the natural numbers.
    6.10  
    6.11  The original theory "IntPrimes" was by Thomas M. Rasmussen, and
     7.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Tue Oct 07 23:12:08 2014 +0200
     7.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Tue Oct 07 23:29:43 2014 +0200
     7.3 @@ -10,7 +10,7 @@
     7.4  begin
     7.5  
     7.6  text {*
     7.7 -  See \cite{davenport92}. \bigskip
     7.8 +  See @{cite davenport92}. \bigskip
     7.9  *}
    7.10  
    7.11  subsection {* Specification of GCD on nats *}
    7.12 @@ -130,7 +130,7 @@
    7.13  *}
    7.14  
    7.15  lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
    7.16 -    -- {* \cite[page 27]{davenport92} *}
    7.17 +    -- {* @{cite \<open>page 27\<close> davenport92} *}
    7.18    apply (induct m n rule: gcd_induct)
    7.19     apply simp
    7.20    apply (case_tac "k = 0")
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Old_Number_Theory/document/root.bib	Tue Oct 07 23:29:43 2014 +0200
     8.3 @@ -0,0 +1,7 @@
     8.4 +@Book{davenport92,
     8.5 +  author =	 {H. Davenport},
     8.6 +  title = 	 {The Higher Arithmetic},
     8.7 +  publisher = 	 {Cambridge University Press},
     8.8 +  year = 	 1992
     8.9 +}
    8.10 +
     9.1 --- a/src/HOL/ROOT	Tue Oct 07 23:12:08 2014 +0200
     9.2 +++ b/src/HOL/ROOT	Tue Oct 07 23:29:43 2014 +0200
     9.3 @@ -212,7 +212,9 @@
     9.4      Quadratic_Reciprocity
     9.5      Primes
     9.6      Pocklington
     9.7 -  document_files "root.tex"
     9.8 +  document_files
     9.9 +    "root.bib"
    9.10 +    "root.tex"
    9.11  
    9.12  session "HOL-Hoare" in Hoare = HOL +
    9.13    description {*
    10.1 --- a/src/HOL/Wellfounded.thy	Tue Oct 07 23:12:08 2014 +0200
    10.2 +++ b/src/HOL/Wellfounded.thy	Tue Oct 07 23:29:43 2014 +0200
    10.3 @@ -464,7 +464,7 @@
    10.4  
    10.5  text {*
    10.6   Inductive definition of the accessible part @{term "acc r"} of a
    10.7 - relation; see also \cite{paulin-tlca}.
    10.8 + relation; see also @{cite "paulin-tlca"}.
    10.9  *}
   10.10  
   10.11  inductive_set
    11.1 --- a/src/HOL/document/root.bib	Tue Oct 07 23:12:08 2014 +0200
    11.2 +++ b/src/HOL/document/root.bib	Tue Oct 07 23:29:43 2014 +0200
    11.3 @@ -1,3 +1,31 @@
    11.4 +@book{card-book,
    11.5 +  title = {Introduction to {C}ardinal {A}rithmetic},
    11.6 +  author = {M. Holz and K. Steffens and E. Weitz},
    11.7 +  publisher = "Birkh{\"{a}}user",
    11.8 +  year = 1999,
    11.9 +}
   11.10 +
   11.11 +@Book{davenport92,
   11.12 +  author =	 {H. Davenport},
   11.13 +  title = 	 {The Higher Arithmetic},
   11.14 +  publisher = 	 {Cambridge University Press},
   11.15 +  year = 	 1992
   11.16 +}
   11.17 +
   11.18 +@InProceedings{paulin-tlca,
   11.19 +  author	= {Christine Paulin-Mohring},
   11.20 +  title		= {Inductive Definitions in the System {Coq}: Rules and
   11.21 +		 Properties},
   11.22 +  crossref	= {tlca93},
   11.23 +  pages		= {328-345}}
   11.24 +
   11.25 +@Proceedings{tlca93,
   11.26 +  title		= {Typed Lambda Calculi and Applications},
   11.27 +  booktitle	= {Typed Lambda Calculi and Applications},
   11.28 +  editor	= {M. Bezem and J.F. Groote},
   11.29 +  year		= 1993,
   11.30 +  publisher	= {Springer},
   11.31 +  series	= {LNCS 664}}
   11.32  
   11.33  @book{Birkhoff79,
   11.34    author =      {Garret Birkhoff},
    12.1 --- a/src/ZF/Induct/Acc.thy	Tue Oct 07 23:12:08 2014 +0200
    12.2 +++ b/src/ZF/Induct/Acc.thy	Tue Oct 07 23:29:43 2014 +0200
    12.3 @@ -8,7 +8,7 @@
    12.4  theory Acc imports Main begin
    12.5  
    12.6  text {*
    12.7 -  Inductive definition of @{text "acc(r)"}; see \cite{paulin-tlca}.
    12.8 +  Inductive definition of @{text "acc(r)"}; see @{cite "paulin-tlca"}.
    12.9  *}
   12.10  
   12.11  consts
    13.1 --- a/src/ZF/Induct/Comb.thy	Tue Oct 07 23:12:08 2014 +0200
    13.2 +++ b/src/ZF/Induct/Comb.thy	Tue Oct 07 23:29:43 2014 +0200
    13.3 @@ -10,7 +10,7 @@
    13.4  text {*
    13.5    Curiously, combinators do not include free variables.
    13.6  
    13.7 -  Example taken from \cite{camilleri-melham}.
    13.8 +  Example taken from @{cite camilleri92}.
    13.9  *}
   13.10  
   13.11  subsection {* Definitions *}
    14.1 --- a/src/ZF/Induct/ListN.thy	Tue Oct 07 23:12:08 2014 +0200
    14.2 +++ b/src/ZF/Induct/ListN.thy	Tue Oct 07 23:29:43 2014 +0200
    14.3 @@ -9,7 +9,7 @@
    14.4  
    14.5  text {*
    14.6    Inductive definition of lists of @{text n} elements; see
    14.7 -  \cite{paulin-tlca}.
    14.8 +  @{cite "paulin-tlca"}.
    14.9  *}
   14.10  
   14.11  consts listn :: "i=>i"
    15.1 --- a/src/ZF/Induct/Primrec.thy	Tue Oct 07 23:12:08 2014 +0200
    15.2 +++ b/src/ZF/Induct/Primrec.thy	Tue Oct 07 23:29:43 2014 +0200
    15.3 @@ -8,7 +8,7 @@
    15.4  theory Primrec imports Main begin
    15.5  
    15.6  text {*
    15.7 -  Proof adopted from \cite{szasz}.
    15.8 +  Proof adopted from \cite{szasz93}.
    15.9  
   15.10    See also \cite[page 250, exercise 11]{mendelson}.
   15.11  *}
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/ZF/Induct/document/root.bib	Tue Oct 07 23:29:43 2014 +0200
    16.3 @@ -0,0 +1,29 @@
    16.4 +@InProceedings{paulin-tlca,
    16.5 +  author	= {Christine Paulin-Mohring},
    16.6 +  title		= {Inductive Definitions in the System {Coq}: Rules and
    16.7 +		 Properties},
    16.8 +  crossref	= {tlca93},
    16.9 +  pages		= {328-345}}
   16.10 +
   16.11 +@Proceedings{tlca93,
   16.12 +  title		= {Typed Lambda Calculi and Applications},
   16.13 +  booktitle	= {Typed Lambda Calculi and Applications},
   16.14 +  editor	= {M. Bezem and J.F. Groote},
   16.15 +  year		= 1993,
   16.16 +  publisher	= {Springer},
   16.17 +  series	= {LNCS 664}}
   16.18 +
   16.19 +@InCollection{szasz93,
   16.20 +  author	= {Nora Szasz},
   16.21 +  title		= {A Machine Checked Proof that {Ackermann's} Function is not
   16.22 +		  Primitive Recursive},
   16.23 +  crossref	= {huet-plotkin93},
   16.24 +  pages		= {317-338}}
   16.25 +
   16.26 +@book{huet-plotkin93,
   16.27 +  editor	= {{G{\'e}rard} Huet and Gordon Plotkin},
   16.28 +  title		= {Logical Environments},
   16.29 +  booktitle	= {Logical Environments},
   16.30 +  publisher	= CUP,
   16.31 +  year		= 1993}
   16.32 +
    17.1 --- a/src/ZF/ROOT	Tue Oct 07 23:12:08 2014 +0200
    17.2 +++ b/src/ZF/ROOT	Tue Oct 07 23:29:43 2014 +0200
    17.3 @@ -174,7 +174,9 @@
    17.4  
    17.5      Comb            (*Combinatory Logic example*)
    17.6      Primrec         (*Primitive recursive functions*)
    17.7 -  document_files "root.tex"
    17.8 +  document_files
    17.9 +    "root.bib"
   17.10 +    "root.tex"
   17.11  
   17.12  session "ZF-Resid" in Resid = ZF +
   17.13    description {*