diff -r b4f18ac786fa -r b98909faaea8 src/HOL/Extraction/document/root.bib
--- a/src/HOL/Extraction/document/root.bib	Mon Sep 06 13:22:11 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-@Article{Berger-JAR-2001,
-  author =       {Ulrich Berger and Helmut Schwichtenberg and Monika Seisenberger},
-  title =        {The {Warshall} Algorithm and {Dickson's} Lemma: Two
-                  Examples of Realistic Program Extraction},
-  journal =      {Journal of Automated Reasoning},
-  publisher =    {Kluwer Academic Publishers},
-  year =         2001,
-  volume =       26,
-  pages =        {205--221}
-}
-
-@TechReport{Coquand93,
-  author = 	 {Thierry Coquand and Daniel Fridlender},
-  title = 	 {A proof of {Higman's} lemma by structural induction},
-  institution =  {Chalmers University},
-  year = 	 1993,
-  month =	 {November}
-}
-
-@InProceedings{Nogin-ENTCS-2000,
-  author = 	 {Aleksey Nogin},
-  title = 	 {Writing constructive proofs yielding efficient extracted programs},
-  booktitle = 	 {Proceedings of the Workshop on Type-Theoretic Languages: Proof Search and Semantics},
-  year =	 2000,
-  editor =	 {Didier Galmiche},
-  volume =	 37,
-  series = 	 {Electronic Notes in Theoretical Computer Science},
-  publisher =	 {Elsevier Science Publishers}
-}
-
-@Article{Wenzel-Wiedijk-JAR2002,
-  author = 	 {Markus Wenzel and Freek Wiedijk},
-  title = 	 {A comparison of the mathematical proof languages {M}izar and {I}sar},
-  journal = 	 {Journal of Automated Reasoning},
-  year = 	 2002,
-  volume =	 29,
-  number =	 {3-4},
-  pages =	 {389-411}
-}