src/HOL/IsaMakefile
changeset 31719 29f5b20e8ee8
parent 31706 1db0c8f235fb
child 31726 ffd2dc631d88
     1.1 --- a/src/HOL/IsaMakefile	Fri Jun 19 18:01:09 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jun 19 18:33:10 2009 +0200
     1.3 @@ -34,6 +34,7 @@
     1.4    HOL-Modelcheck \
     1.5    HOL-NanoJava \
     1.6    HOL-Nominal-Examples \
     1.7 +  HOL-NewNumberTheory \
     1.8    HOL-NumberTheory \
     1.9    HOL-Prolog \
    1.10    HOL-SET-Protocol \
    1.11 @@ -489,6 +490,18 @@
    1.12  	@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
    1.13  
    1.14  
    1.15 +## HOL-NewNumberTheory
    1.16 +
    1.17 +HOL-NewNumberTheory: HOL $(LOG)/HOL-NewNumberTheory.gz
    1.18 +
    1.19 +$(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL GCD.thy Library/Multiset.thy	\
    1.20 +  NewNumberTheory/Fib.thy NewNumberTheory/Binomial.thy			\
    1.21 +  NewNumberTheory/Residues.thy NewNumberTheory/UniqueFactorization.thy  \
    1.22 +  NewNumberTheory/Cong.thy NewNumberTheory/MiscAlgebra.thy \
    1.23 +  NewNumberTheory/ROOT.ML
    1.24 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NewNumberTheory
    1.25 +
    1.26 +
    1.27  ## HOL-NumberTheory
    1.28  
    1.29  HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz