--- a/src/HOL/Extraction/document/root.bib Tue Sep 07 11:51:53 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}
-}