--- a/src/HOL/IsaMakefile Tue Nov 13 10:58:46 2007 +0100
+++ b/src/HOL/IsaMakefile Tue Nov 13 10:59:26 2007 +0100
@@ -625,8 +625,9 @@
HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/Efficient_Nat.thy \
- Extraction/Higman.thy Extraction/ROOT.ML Extraction/Pigeonhole.thy \
- Extraction/QuotRem.thy \
+ Extraction/Euclid.thy Extraction/Greatest_Common_Divisor.thy \
+ Extraction/Higman.thy Extraction/Pigeonhole.thy Extraction/QuotRem.thy \
+ Extraction/ROOT.ML Extraction/Util.thy \
Extraction/Warshall.thy Extraction/document/root.tex \
Extraction/document/root.bib
@$(ISATOOL) usedir $(OUT)/HOL Extraction