# HG changeset patch
# User mueller
# Date 862394303 -7200
# Node ID 2ea678d3523f69083c052be5d54c3ec253015414
# Parent  984866a8f905797dd57e922e19b4f3d5590d1013
removed (most of) IOA (see HOLCF/IOA);

diff -r 984866a8f905 -r 2ea678d3523f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Apr 30 11:56:17 1997 +0200
+++ b/src/HOL/IsaMakefile	Wed Apr 30 11:58:23 1997 +0200
@@ -71,24 +71,14 @@
 	@$(ISATOOL) usedir $(OUT)/HOL Integ
 
 
-## I/O Automata
+## I/O Automata (meta theory only)
 
-IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet \
-		Receiver Sender
-IOA_ABP_NAMES = Action Correctness Lemmas
-IOA_MT_NAMES = Asig IOA Solve
 
-IOA_FILES = IOA/NTP/ROOT.ML IOA/ABP/ROOT.ML IOA/NTP/Spec.thy \
- $(IOA_NTP_NAMES:%=IOA/NTP/%.thy) $(IOA_NTP_NAMES:%=IOA/NTP/%.ML) \
- IOA/ABP/Abschannel.thy IOA/ABP/Abschannel_finite.thy IOA/ABP/Env.thy \
- IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy IOA/ABP/Packet.thy \
- IOA/ABP/Receiver.thy IOA/ABP/Sender.thy IOA/ABP/Spec.thy \
- $(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML) \
- $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
+IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \
+  IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML
 
-IOA:	$(OUT)/HOL $(IOA_FILES)
-	@$(ISATOOL) usedir -s IOA-NTP $(OUT)/HOL IOA/NTP
-	@$(ISATOOL) usedir -s IOA-ABP $(OUT)/HOL IOA/ABP
+IOA: $(OUT)/HOL $(IOA_FILES)
+	@$(ISATOOL) usedir $(OUT)/HOL IOA
 
 
 ## Authentication & Security Protocols
diff -r 984866a8f905 -r 2ea678d3523f src/HOL/Makefile
--- a/src/HOL/Makefile	Wed Apr 30 11:56:17 1997 +0200
+++ b/src/HOL/Makefile	Wed Apr 30 11:58:23 1997 +0200
@@ -121,30 +121,6 @@
 	else echo 'exit_use_dir"Integ";quit();' | $(LOGIC); \
 	fi
 
-##I/O Automata
-IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet\
-		Receiver Sender
-IOA_ABP_NAMES = Action Correctness Lemmas
-IOA_MT_NAMES = Asig IOA Solve
-
-IOA_FILES = IOA/NTP/ROOT.ML IOA/ABP/ROOT.ML IOA/NTP/Spec.thy\
- $(IOA_NTP_NAMES:%=IOA/NTP/%.thy) $(IOA_NTP_NAMES:%=IOA/NTP/%.ML)\
- IOA/ABP/Abschannel.thy IOA/ABP/Abschannel_finite.thy IOA/ABP/Env.thy\
- IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy IOA/ABP/Packet.thy\
- IOA/ABP/Receiver.thy IOA/ABP/Sender.thy IOA/ABP/Spec.thy\
- $(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML)\
- $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
-
-IOA:	$(BIN)/HOL  $(IOA_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"IOA/NTP";quit();' \
-	       | $(LOGIC);\
-	     echo 'make_html := true; exit_use_dir"IOA/ABP";quit();' \
-	       | $(LOGIC);\
-	else echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC); \
-	     echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC); \
-	fi
-
 
 ##Authentication & Security Protocols
 Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
@@ -238,7 +214,7 @@
 	fi
 
 #Full test.
-test:	$(BIN)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
+test:	$(BIN)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda MiniML ex
 	echo 'Test examples ran successfully' > test
 
 .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL