1.1 --- a/src/HOLCF/IsaMakefile	Mon Mar 17 15:09:13 1997 +0100
     1.2 +++ b/src/HOLCF/IsaMakefile	Mon Mar 17 15:37:16 1997 +0100
     1.3 @@ -33,6 +33,14 @@
     1.4  
     1.5  #### Tests and examples
     1.6  
     1.7 +## IMP
     1.8 +
     1.9 +IMP_THYS = IMP/Denotational.thy
    1.10 +IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
    1.11 +
    1.12 +IMP:	$(OUT)/HOLCF $(IMP_FILES)
    1.13 +	@$(ISATOOL) testdir $(OUT)/HOLCF IMP
    1.14 +
    1.15  ## Miscellaneous examples
    1.16  
    1.17  EX_THYS = ex/Classlib.thy ex/Witness.thy\
    1.18 @@ -42,7 +50,12 @@
    1.19  
    1.20  EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
    1.21  
    1.22 -test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES)
    1.23 +EX:	ex/ROOT.ML $(EX_FILES)
    1.24  	@$(ISATOOL) testdir $(OUT)/HOLCF ex
    1.25  
    1.26 +## Full test
    1.27 +
    1.28 +test:	$(OUT)/HOLCF IMP EX
    1.29 +	echo 'Test examples ran successfully' > test
    1.30 +
    1.31  .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF