# HG changeset patch
# User berghofe
# Date 1123264618 -7200
# Node ID 7425bf9f0f4bd649c8558483ca4742ab3a0c6715
# Parent  b257300c3a9c7c0a2900a10fbb05a66517142b47
Added Extraction/Pigeonhole.

diff -r b257300c3a9c -r 7425bf9f0f4b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Aug 05 12:20:30 2005 +0200
+++ b/src/HOL/IsaMakefile	Fri Aug 05 19:56:58 2005 +0200
@@ -535,7 +535,8 @@
 HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
 
 $(LOG)/HOL-Extraction.gz: $(OUT)/HOL \
-  Extraction/Higman.thy Extraction/ROOT.ML Extraction/QuotRem.thy \
+  Extraction/Higman.thy Extraction/ROOT.ML Extraction/Pigeonhole.thy \
+  Extraction/QuotRem.thy \
   Extraction/Warshall.thy Extraction/document/root.tex \
   Extraction/document/root.bib
 	@$(ISATOOL) usedir $(OUT)/HOL Extraction