# HG changeset patch
# User clasohm
# Date 783786373 -3600
# Node ID 45d0cf6e309d0d49939b6933325766787d92b290
# Parent  fd1be45b64bfeedf63b66cb5f5d59185edf1f9db
added IOA files

diff -r fd1be45b64bf -r 45d0cf6e309d Makefile
--- 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