--- 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},