--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Tue Oct 07 23:29:43 2014 +0200
@@ -826,7 +826,7 @@
theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
does not increase cardinality -- the proof of this fact adapts a standard
set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
-at page 47 in \cite{card-book}. Then everything else follows fairly easily. *}
+at page 47 in @{cite "card-book"}. Then everything else follows fairly easily. *}
lemma infinite_iff_card_of_nat:
"\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
--- a/src/HOL/GCD.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/GCD.thy Tue Oct 07 23:29:43 2014 +0200
@@ -8,7 +8,7 @@
This file combines and revises a number of prior developments.
The original theories "GCD" and "Primes" were by Christophe Tabacznyj
-and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
+and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
gcd, lcm, and prime for the natural numbers.
The original theory "IntPrimes" was by Thomas M. Rasmussen, and
@@ -364,7 +364,7 @@
*}
lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
- -- {* \cite[page 27]{davenport92} *}
+ -- {* @{cite \<open>page 27\<close> davenport92} *}
apply (induct m n rule: gcd_nat_induct)
apply simp
apply (case_tac "k = 0")
--- a/src/HOL/Induct/Comb.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/Induct/Comb.thy Tue Oct 07 23:29:43 2014 +0200
@@ -10,7 +10,7 @@
text {*
Curiously, combinators do not include free variables.
- Example taken from \cite{camilleri-melham}.
+ Example taken from @{cite camilleri92}.
HOL system proofs may be found in the HOL distribution at
.../contrib/rule-induction/cl.ml
--- a/src/HOL/Main.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/Main.thy Tue Oct 07 23:29:43 2014 +0200
@@ -10,7 +10,7 @@
complex numbers etc.
*}
-text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
+text {* See further @{cite "Nipkow-et-al:2002:tutorial"} *}
no_notation
bot ("\<bottom>") and
--- a/src/HOL/Number_Theory/Cong.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/Number_Theory/Cong.thy Tue Oct 07 23:29:43 2014 +0200
@@ -8,7 +8,7 @@
This file combines and revises a number of prior developments.
The original theories "GCD" and "Primes" were by Christophe Tabacznyj
-and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
+and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
gcd, lcm, and prime for the natural numbers.
The original theory "IntPrimes" was by Thomas M. Rasmussen, and
--- a/src/HOL/Number_Theory/Primes.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/Number_Theory/Primes.thy Tue Oct 07 23:29:43 2014 +0200
@@ -8,7 +8,7 @@
This file combines and revises a number of prior developments.
The original theories "GCD" and "Primes" were by Christophe Tabacznyj
-and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
+and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
gcd, lcm, and prime for the natural numbers.
The original theory "IntPrimes" was by Thomas M. Rasmussen, and
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Tue Oct 07 23:29:43 2014 +0200
@@ -10,7 +10,7 @@
begin
text {*
- See \cite{davenport92}. \bigskip
+ See @{cite davenport92}. \bigskip
*}
subsection {* Specification of GCD on nats *}
@@ -130,7 +130,7 @@
*}
lemma gcd_mult_distrib2: "k * gcd m n = gcd (k * m) (k * n)"
- -- {* \cite[page 27]{davenport92} *}
+ -- {* @{cite \<open>page 27\<close> davenport92} *}
apply (induct m n rule: gcd_induct)
apply simp
apply (case_tac "k = 0")
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Old_Number_Theory/document/root.bib Tue Oct 07 23:29:43 2014 +0200
@@ -0,0 +1,7 @@
+@Book{davenport92,
+ author = {H. Davenport},
+ title = {The Higher Arithmetic},
+ publisher = {Cambridge University Press},
+ year = 1992
+}
+
--- a/src/HOL/ROOT Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/ROOT Tue Oct 07 23:29:43 2014 +0200
@@ -212,7 +212,9 @@
Quadratic_Reciprocity
Primes
Pocklington
- document_files "root.tex"
+ document_files
+ "root.bib"
+ "root.tex"
session "HOL-Hoare" in Hoare = HOL +
description {*
--- a/src/HOL/Wellfounded.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/Wellfounded.thy Tue Oct 07 23:29:43 2014 +0200
@@ -464,7 +464,7 @@
text {*
Inductive definition of the accessible part @{term "acc r"} of a
- relation; see also \cite{paulin-tlca}.
+ relation; see also @{cite "paulin-tlca"}.
*}
inductive_set
--- a/src/HOL/document/root.bib Tue Oct 07 23:12:08 2014 +0200
+++ b/src/HOL/document/root.bib Tue Oct 07 23:29:43 2014 +0200
@@ -1,3 +1,31 @@
+@book{card-book,
+ title = {Introduction to {C}ardinal {A}rithmetic},
+ author = {M. Holz and K. Steffens and E. Weitz},
+ publisher = "Birkh{\"{a}}user",
+ year = 1999,
+}
+
+@Book{davenport92,
+ author = {H. Davenport},
+ title = {The Higher Arithmetic},
+ publisher = {Cambridge University Press},
+ year = 1992
+}
+
+@InProceedings{paulin-tlca,
+ author = {Christine Paulin-Mohring},
+ title = {Inductive Definitions in the System {Coq}: Rules and
+ Properties},
+ crossref = {tlca93},
+ pages = {328-345}}
+
+@Proceedings{tlca93,
+ title = {Typed Lambda Calculi and Applications},
+ booktitle = {Typed Lambda Calculi and Applications},
+ editor = {M. Bezem and J.F. Groote},
+ year = 1993,
+ publisher = {Springer},
+ series = {LNCS 664}}
@book{Birkhoff79,
author = {Garret Birkhoff},
--- a/src/ZF/Induct/Acc.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/ZF/Induct/Acc.thy Tue Oct 07 23:29:43 2014 +0200
@@ -8,7 +8,7 @@
theory Acc imports Main begin
text {*
- Inductive definition of @{text "acc(r)"}; see \cite{paulin-tlca}.
+ Inductive definition of @{text "acc(r)"}; see @{cite "paulin-tlca"}.
*}
consts
--- a/src/ZF/Induct/Comb.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/ZF/Induct/Comb.thy Tue Oct 07 23:29:43 2014 +0200
@@ -10,7 +10,7 @@
text {*
Curiously, combinators do not include free variables.
- Example taken from \cite{camilleri-melham}.
+ Example taken from @{cite camilleri92}.
*}
subsection {* Definitions *}
--- a/src/ZF/Induct/ListN.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/ZF/Induct/ListN.thy Tue Oct 07 23:29:43 2014 +0200
@@ -9,7 +9,7 @@
text {*
Inductive definition of lists of @{text n} elements; see
- \cite{paulin-tlca}.
+ @{cite "paulin-tlca"}.
*}
consts listn :: "i=>i"
--- a/src/ZF/Induct/Primrec.thy Tue Oct 07 23:12:08 2014 +0200
+++ b/src/ZF/Induct/Primrec.thy Tue Oct 07 23:29:43 2014 +0200
@@ -8,7 +8,7 @@
theory Primrec imports Main begin
text {*
- Proof adopted from \cite{szasz}.
+ Proof adopted from \cite{szasz93}.
See also \cite[page 250, exercise 11]{mendelson}.
*}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/document/root.bib Tue Oct 07 23:29:43 2014 +0200
@@ -0,0 +1,29 @@
+@InProceedings{paulin-tlca,
+ author = {Christine Paulin-Mohring},
+ title = {Inductive Definitions in the System {Coq}: Rules and
+ Properties},
+ crossref = {tlca93},
+ pages = {328-345}}
+
+@Proceedings{tlca93,
+ title = {Typed Lambda Calculi and Applications},
+ booktitle = {Typed Lambda Calculi and Applications},
+ editor = {M. Bezem and J.F. Groote},
+ year = 1993,
+ publisher = {Springer},
+ series = {LNCS 664}}
+
+@InCollection{szasz93,
+ author = {Nora Szasz},
+ title = {A Machine Checked Proof that {Ackermann's} Function is not
+ Primitive Recursive},
+ crossref = {huet-plotkin93},
+ pages = {317-338}}
+
+@book{huet-plotkin93,
+ editor = {{G{\'e}rard} Huet and Gordon Plotkin},
+ title = {Logical Environments},
+ booktitle = {Logical Environments},
+ publisher = CUP,
+ year = 1993}
+
--- a/src/ZF/ROOT Tue Oct 07 23:12:08 2014 +0200
+++ b/src/ZF/ROOT Tue Oct 07 23:29:43 2014 +0200
@@ -174,7 +174,9 @@
Comb (*Combinatory Logic example*)
Primrec (*Primitive recursive functions*)
- document_files "root.tex"
+ document_files
+ "root.bib"
+ "root.tex"
session "ZF-Resid" in Resid = ZF +
description {*