# HG changeset patch
# User berghofe
# Date 1027338944 -7200
# Node ID 024af54a625c9fea2fd57b84a4ddc645396c7f6e
# Parent  d128b5915f6b524a04e0e255e61b354e9c6980fc
Added "nocite" to avoid BibTeX error when proofs are switched off.

diff -r d128b5915f6b -r 024af54a625c src/HOL/Extraction/document/root.tex
--- 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