--- a/Makefile Wed Aug 31 16:25:19 1994 +0200
+++ b/Makefile Wed Aug 31 17:50:59 1994 +0200
@@ -31,6 +31,9 @@
../Provers/classical.ML ../Provers/simplifier.ML \
../Provers/splitter.ML ../Provers/ind.ML
+IMP_FILES = IMP/ROOT.ML IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\
+ IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy
+
EX_FILES = ex/ROOT.ML ex/cla.ML \
ex/LexProd.ML ex/LexProd.thy ex/meson.ML ex/mesontest.ML\
ex/MT.ML ex/MT.thy ex/Acc.ML ex/Acc.thy \
@@ -64,13 +67,13 @@
$(BIN)/Pure:
cd ../Pure; $(MAKE)
-#Directory Subst also tests the system
+#Directories IMP and Subst also test the system
#Load ex/ROOT.ML last since it creates the file "test"
-test: $(BIN)/HOL $(SUBST_FILES) $(EX_FILES)
+test: $(BIN)/HOL $(IMP_FILES) $(SUBST_FILES) $(EX_FILES)
case "$(COMP)" in \
- poly*) echo 'use"Subst/ROOT.ML"; use"ex/ROOT.ML"; quit();' \
+ poly*) echo 'use"IMP/ROOT.ML"; use"Subst/ROOT.ML"; use"ex/ROOT.ML"; quit();' \
| $(COMP) $(BIN)/HOL ;;\
- sml*) echo 'use"Subst/ROOT.ML"; use"ex/ROOT.ML";' | $(BIN)/HOL;;\
+ sml*) echo 'use"IMP/ROOT.ML"; use"Subst/ROOT.ML"; use"ex/ROOT.ML";' | $(BIN)/HOL;;\
*) echo Bad value for ISABELLECOMP: \
$(COMP) is not poly or sml;;\
esac