# HG changeset patch
# User wenzelm
# Date 1125495999 -7200
# Node ID d364e0fd9c2f89b102c729863fbc5fb7e73a9215
# Parent  3bdf1dfcdee43fa40786da4a5f117a0274127cbe
added Avigad-Donnelly;

diff -r 3bdf1dfcdee4 -r d364e0fd9c2f src/HOL/Library/Library/document/root.bib
--- a/src/HOL/Library/Library/document/root.bib	Wed Aug 31 15:46:38 2005 +0200
+++ b/src/HOL/Library/Library/document/root.bib	Wed Aug 31 15:46:39 2005 +0200
@@ -1,5 +1,15 @@
 
- @Unpublished{Abrial-Laffitte,
+ @InProceedings{Avigad-Donnelly,
+  author = 	 {Jeremy Avigad and Kevin Donnelly},
+  title = 	 {Formalizing {O} notation in {Isabelle/HOL}},
+  booktitle = 	 {Automated Reasoning: second international conference, IJCAR 2004},
+  pages =	 {357--371},
+  year =	 2004,
+  editor =	 {David Basin and Micha\"el Rusiowitch},
+  publisher =	 {Springer}
+}
+
+@Unpublished{Abrial-Laffitte,
   author = 	 {Abrial and Laffitte},
   title = 	 {Towards the Mechanization of the Proofs of
                   Some Classical Theorems of Set Theory},