summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 07 Oct 2014 23:29:43 +0200 | |

changeset 58623 | 2db1df2c8467 |

parent 58622 | aa99568f56de |

child 58624 | 75b9b64ccb58 |

more bibtex entries;
more antiquotations;

--- 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 {*