src/HOL/IsaMakefile
changeset 8179 6a0b1037bab3
parent 8177 e59e93ad85eb
child 8193 33e4ec7a2daa
     1.1 --- a/src/HOL/IsaMakefile	Tue Feb 01 12:26:47 2000 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Feb 01 18:18:09 2000 +0100
     1.3 @@ -151,6 +151,16 @@
     1.4  	@$(ISATOOL) usedir $(OUT)/HOL IMP
     1.5  
     1.6  
     1.7 +## HOL-IMPP
     1.8 +
     1.9 +HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz
    1.10 +
    1.11 +$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy IMPP/Com.ML \
    1.12 +  IMPP/Natural.thy IMPP/Natural.ML IMPP/Hoare.thy IMPP/Hoare.ML \
    1.13 +  IMPP/Misc.thy IMPP/Misc.ML IMPP/EvenOdd.thy IMPP/EvenOdd.ML
    1.14 +	@$(ISATOOL) usedir $(OUT)/HOL IMPP
    1.15 +
    1.16 +
    1.17  ## HOL-Hoare
    1.18  
    1.19  HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
    1.20 @@ -478,8 +488,9 @@
    1.21  
    1.22  clean:
    1.23  	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \
    1.24 -	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \
    1.25 -	  $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.26 +	  $(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
    1.27 +	  $(LOG)/HOL-Induct.gz $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
    1.28 +	  $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.29  	  $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
    1.30  	  $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-BCV.gz $(LOG)/HOL-IOA.gz \
    1.31  	  $(LOG)/HOL-AxClasses-Group.gz		\