src/HOLCF/IsaMakefile

 #
 
 #### Base system
 
 OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
 
 THYS = Porder.thy Porder0.thy Pcpo.thy \
        Fun1.thy Fun2.thy Fun3.thy \
        Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
        Cprod1.thy Cprod2.thy Cprod3.thy \

   IOA/NTP/Receiver.ML IOA/NTP/Receiver.thy \
   IOA/NTP/Sender.ML IOA/NTP/Sender.thy \
   IOA/NTP/Spec.thy 
 
  
-IOA: $(OUT)/HOLCF $(IOA_FILES)
+$(OUT)/IOA: $(OUT)/HOLCF $(IOA_FILES)
 	@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA
 
-IOA_ABP: $(OUT)/IOA $(IOA_ABP_FILES)
+$(LOG)/IOA-ABP.gz: $(OUT)/IOA $(IOA_ABP_FILES)
 	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP
 
-IOA_NTP: $(OUT)/IOA $(IOA_NTP_FILES)
+$(LOG)/IOA-NTP.gz: $(OUT)/IOA $(IOA_NTP_FILES)
 	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP
 
 
 ## IMP
 
 IMP_THYS = IMP/Denotational.thy
 IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
 
-IMP:	$(OUT)/HOLCF $(IMP_FILES)
+$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF $(IMP_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
 
 
 ## Miscellaneous examples
 

 	  ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy \
 	  ex/Hoare.thy ex/Loop.thy
 
 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
 
-ex:	ex/ROOT.ML $(EX_FILES)
+$(LOG)/HOLCF-ex.gz: ex/ROOT.ML $(EX_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOLCF ex
 
 
 ## Full test
 
-test:	$(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP ex
-	echo 'Test examples ran successfully' > test
+ALL_TARGETS = $(OUT)/HOLCF $(OUT)/IOA $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
+  $(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz
+
+test: $(ALL_TARGETS)
+
+clean:
+	@rm -f $(ALL_TARGETS)
 
 
 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF