Added new program extraction examples.
authorberghofe
Tue, 13 Nov 2007 10:59:26 +0100
changeset 25423 2c6167e2c587
parent 25422 37e991068d96
child 25424 170f4cc34697
Added new program extraction examples.
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