--- a/src/HOL/Extraction/document/root.bib Fri Aug 05 19:57:57 2005 +0200
+++ b/src/HOL/Extraction/document/root.bib Fri Aug 05 19:58:30 2005 +0200
@@ -16,3 +16,14 @@
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}
+}