Added "nocite" to avoid BibTeX error when proofs are switched off.

--- a/src/HOL/Extraction/document/root.tex	Sun Jul 21 15:52:39 2002 +0200
+++ b/src/HOL/Extraction/document/root.tex	Mon Jul 22 13:55:44 2002 +0200
@@ -11,6 +11,8 @@
 \author{Stefan Berghofer}
 \maketitle
 
+\nocite{Berger-JAR-2001,Coquand93}
+
 \tableofcontents
 
 \parindent 0pt\parskip 0.5ex