# HG changeset patch
# User berghofe
# Date 1194947966 -3600
# Node ID 2c6167e2c5876217deae359d6f59e7f37e026428
# Parent  37e991068d9642e6fb61c9e12a3e380c133c740d
Added new program extraction examples.

diff -r 37e991068d96 -r 2c6167e2c587 src/HOL/IsaMakefile
--- 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