src/HOL/IsaMakefile
changeset 14626 dfb8d2977263
parent 14610 9c2e31e483b2
child 14641 79b7bd936264
     1.1 --- a/src/HOL/IsaMakefile	Mon Apr 19 09:27:27 2004 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Apr 19 09:31:00 2004 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  ## targets
     1.5  
     1.6  default: HOL
     1.7 -images: HOL HOL-Algebra HOL-Complex TLA
     1.8 +images: HOL HOL-Algebra HOL-Complex TLA HOL4
     1.9  
    1.10  #Note: keep targets sorted (except for HOL-Library)
    1.11  test: \
    1.12 @@ -264,7 +264,7 @@
    1.13  
    1.14  ## HOL-Import-HOL
    1.15  
    1.16 -HOL-Import-HOL: HOL-Complex $(LOG)/HOL-Import-HOL.gz
    1.17 +HOL4: HOL-Complex $(LOG)/HOL4.gz
    1.18  
    1.19  HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \
    1.20    bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \
    1.21 @@ -276,11 +276,11 @@
    1.22    seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \
    1.23    word_base.imp word_bitop.imp word_num.imp
    1.24  
    1.25 -$(LOG)/HOL-Import-HOL.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES) \
    1.26 +$(LOG)/HOL4.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES) \
    1.27    $(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \
    1.28    Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy Import/HOL/HOL4Vec.thy \
    1.29    Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy Import/HOL/ROOT.ML
    1.30 -	@cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOL-Import-HOL
    1.31 +	@cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOL4
    1.32  
    1.33  
    1.34  ## HOL-NumberTheory