diff -r 0f3ee1f89ca8 -r dbcb1a6c92e1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Aug 03 10:52:30 2000 +0200
+++ b/src/HOL/IsaMakefile	Thu Aug 03 10:53:06 2000 +0200
@@ -9,7 +9,8 @@
 default: HOL
 images: HOL HOL-Real TLA
 test: HOL-Isar_examples HOL-Induct HOL-ex HOL-Subst HOL-IMP HOL-IMPP \
-  HOL-Hoare HOL-Lex HOL-Algebra HOL-Auth HOL-UNITY HOL-Modelcheck \
+  HOL-NumberTheory HOL-Hoare HOL-Lex HOL-Algebra \
+  HOL-Auth HOL-UNITY HOL-Modelcheck \
   HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV HOL-MicroJava \
   HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
   HOL-AxClasses-Tutorial HOL-Real-ex \
@@ -48,9 +49,11 @@
   $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml	\
   Arith.ML Arith.thy Calculation.thy Datatype.thy Divides.ML		\
   Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy	\
-  HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML		\
-  Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML	\
-  Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML	\
+  HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy \
+  Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy \
+  Integ/IntArith.ML Integ/IntArith.thy \
+  Integ/IntPower.ML Integ/IntPower.thy \
+  Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML	\
   Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML	\
   Integ/NatBin.thy Integ/NatSimprocs.thy Integ/NatSimprocs.ML		\
   Integ/int_arith1.ML Integ/int_arith2.ML Integ/nat_simprocs.ML         \
@@ -167,6 +170,22 @@
 	@$(ISATOOL) usedir $(OUT)/HOL IMPP
 
 
+## HOL-NumberTheory
+
+HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz
+
+$(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \
+  NumberTheory/BijectionRel.ML NumberTheory/BijectionRel.thy \
+  NumberTheory/Chinese.ML NumberTheory/Chinese.thy \
+  NumberTheory/EulerFermat.ML NumberTheory/EulerFermat.thy \
+  NumberTheory/IntFact.ML NumberTheory/IntFact.thy \
+  NumberTheory/IntPrimes.ML NumberTheory/IntPrimes.thy \
+  NumberTheory/WilsonBij.ML NumberTheory/WilsonBij.thy \
+  NumberTheory/WilsonRuss.ML NumberTheory/WilsonRuss.thy \
+  NumberTheory/ROOT.ML
+	@$(ISATOOL) usedir $(OUT)/HOL NumberTheory
+
+
 ## HOL-Hoare
 
 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz