diff -r 7715d4d3586f -r 29f5b20e8ee8 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jun 19 18:01:09 2009 +0200
+++ b/src/HOL/IsaMakefile	Fri Jun 19 18:33:10 2009 +0200
@@ -34,6 +34,7 @@
   HOL-Modelcheck \
   HOL-NanoJava \
   HOL-Nominal-Examples \
+  HOL-NewNumberTheory \
   HOL-NumberTheory \
   HOL-Prolog \
   HOL-SET-Protocol \
@@ -489,6 +490,18 @@
 	@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
 
 
+## HOL-NewNumberTheory
+
+HOL-NewNumberTheory: HOL $(LOG)/HOL-NewNumberTheory.gz
+
+$(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL GCD.thy Library/Multiset.thy	\
+  NewNumberTheory/Fib.thy NewNumberTheory/Binomial.thy			\
+  NewNumberTheory/Residues.thy NewNumberTheory/UniqueFactorization.thy  \
+  NewNumberTheory/Cong.thy NewNumberTheory/MiscAlgebra.thy \
+  NewNumberTheory/ROOT.ML
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NewNumberTheory
+
+
 ## HOL-NumberTheory
 
 HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz