added entry for running HOLLight
authorobua
Mon Sep 26 02:27:59 2005 +0200 (2005-09-26)
changeset 17645940371ea0ff3
parent 17644 bd59bfd4bf37
child 17646 c5a4fe81857e
added entry for running HOLLight
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/IsaMakefile	Mon Sep 26 02:27:14 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Sep 26 02:27:59 2005 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  default: HOL
     1.6  generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
     1.7 -images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix TLA HOL4
     1.8 +images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix TLA
     1.9  
    1.10  #Note: keep targets sorted (except for HOL-Library)
    1.11  test: \
    1.12 @@ -300,6 +300,13 @@
    1.13    Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy Import/HOL/ROOT.ML
    1.14  	@cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOL4
    1.15  
    1.16 +HOLLight: HOL-Complex $(LOG)/HOLLight.gz
    1.17 +
    1.18 +$(LOG)/HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES) \
    1.19 +  Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \
    1.20 +  Import/HOLLight/ROOT.ML
    1.21 +	@cd Import/HOLLight; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOLLight
    1.22 +
    1.23  
    1.24  ## HOL-NumberTheory
    1.25