src/HOL/Library/Library/document/root.bib

--- a/src/HOL/Library/Library/document/root.bib	Tue Feb 27 00:32:52 2007 +0100
+++ b/src/HOL/Library/Library/document/root.bib	Tue Feb 27 00:33:49 2007 +0100
@@ -1,5 +1,12 @@
 
- @InProceedings{Avigad-Donnelly,
+@Unpublished{Abrial-Laffitte,
+  author = 	 {Abrial and Laffitte},
+  title = 	 {Towards the Mechanization of the Proofs of
+                  Some Classical Theorems of Set Theory},
+  note = 	 {Unpublished}
+}
+
+@InProceedings{Avigad-Donnelly,
   author = 	 {Jeremy Avigad and Kevin Donnelly},
   title = 	 {Formalizing {O} notation in {Isabelle/HOL}},
   booktitle = 	 {Automated Reasoning: second international conference, IJCAR 2004},
@@ -9,13 +16,6 @@
   publisher =	 {Springer}
 }
 
-@Unpublished{Abrial-Laffitte,
-  author = 	 {Abrial and Laffitte},
-  title = 	 {Towards the Mechanization of the Proofs of
-                  Some Classical Theorems of Set Theory},
-  note = 	 {Unpublished}
-}
-
 @Book{Oberschelp:1993,
   author =	 {Arnold Oberschelp},
   title = 	 {Rekursionstheorie},
@@ -23,6 +23,21 @@
   year = 	 1993
 }
 
+@InProceedings{Podelski-Rybalchenko,
+  author = 	 {Andreas Podelski and Andrey Rybalchenko},
+  title = 	 {Transition Invariants},
+  booktitle = 	 {19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)},
+  pages =	 {32--41},
+  year =	 2004
+}
+
+@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