diff -r ae4a8446df16 -r b4a6b987aebe src/HOL/Extraction/document/root.bib
--- 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}
+}