Added the HOLCF-based den. sem. of IMP.
authornipkow
Mon, 17 Mar 1997 15:37:16 +0100
changeset 2797 54ca927b831b
parent 2796 c23e367e57be
child 2798 f84be65745b2
Added the HOLCF-based den. sem. of IMP.
src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Mon Mar 17 15:09:13 1997 +0100
+++ b/src/HOLCF/IsaMakefile	Mon Mar 17 15:37:16 1997 +0100
@@ -33,6 +33,14 @@
 
 #### Tests and examples
 
+## IMP
+
+IMP_THYS = IMP/Denotational.thy
+IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
+
+IMP:	$(OUT)/HOLCF $(IMP_FILES)
+	@$(ISATOOL) testdir $(OUT)/HOLCF IMP
+
 ## Miscellaneous examples
 
 EX_THYS = ex/Classlib.thy ex/Witness.thy\
@@ -42,7 +50,12 @@
 
 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
 
-test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES)
+EX:	ex/ROOT.ML $(EX_FILES)
 	@$(ISATOOL) testdir $(OUT)/HOLCF ex
 
+## Full test
+
+test:	$(OUT)/HOLCF IMP EX
+	echo 'Test examples ran successfully' > test
+
 .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF