# HG changeset patch
# User nipkow
# Date 858609436 -3600
# Node ID 54ca927b831bce7bc8cd17d6c0c36cabea6989d1
# Parent  c23e367e57be16a9307ba68b83a2e97db9f2b2d8
Added the HOLCF-based den. sem. of IMP.

diff -r c23e367e57be -r 54ca927b831b 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