--- a/Makefile Wed Nov 02 11:50:09 1994 +0100
+++ b/Makefile Wed Nov 02 15:26:13 1994 +0100
@@ -34,6 +34,19 @@
IMP_FILES = IMP/ROOT.ML IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\
IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy
+IOA_FILES = IOA/ROOT.ML IOA/example/Action.ML IOA/example/Action.thy\
+ IOA/example/Channels.ML IOA/example/Channels.thy\
+ IOA/example/Correctness.ML IOA/example/Correctness.thy\
+ IOA/example/Impl.ML IOA/example/Impl.thy IOA/example/Lemmas.ML\
+ IOA/example/Lemmas.thy IOA/example/Multiset.ML\
+ IOA/example/Multiset.thy IOA/example/Packet.thy\
+ IOA/example/Receiver.ML IOA/example/Receiver.thy\
+ IOA/example/Sender.ML IOA/example/Sender.thy IOA/example/Spec.thy\
+ IOA/meta_theory/Asig.thy IOA/meta_theory/IOA.ML\
+ IOA/meta_theory/IOA.thy IOA/meta_theory/Option.ML\
+ IOA/meta_theory/Option.thy IOA/meta_theory/Solve.ML\
+ IOA/meta_theory/Solve.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 \
@@ -69,11 +82,11 @@
#Directories IMP and Subst also test the system
#Load ex/ROOT.ML last since it creates the file "test"
-test: $(BIN)/HOL $(IMP_FILES) $(SUBST_FILES) $(EX_FILES)
+test: $(BIN)/HOL $(IMP_FILES) $(IOA_FILES) $(SUBST_FILES) $(EX_FILES)
case "$(COMP)" in \
- poly*) echo 'use"IMP/ROOT.ML"; use"Subst/ROOT.ML"; use"ex/ROOT.ML"; quit();' \
+ poly*) echo 'use"IMP/ROOT.ML"; use"IOA/ROOT.ML"; use"Subst/ROOT.ML"; use"ex/ROOT.ML"; quit();' \
| $(COMP) $(BIN)/HOL ;;\
- sml*) echo 'use"IMP/ROOT.ML"; use"Subst/ROOT.ML"; use"ex/ROOT.ML";' | $(BIN)/HOL;;\
+ sml*) echo 'use"IMP/ROOT.ML"; use"IOA/ROOT.ML"; use"Subst/ROOT.ML"; use"ex/ROOT.ML";' | $(BIN)/HOL;;\
*) echo Bad value for ISABELLECOMP: \
$(COMP) is not poly or sml;;\
esac