removed (most of) IOA (see HOLCF/IOA);
authormueller
Wed Apr 30 11:58:23 1997 +0200 (1997-04-30)
changeset 30792ea678d3523f
parent 3078 984866a8f905
child 3080 517b1de05735
removed (most of) IOA (see HOLCF/IOA);
src/HOL/IsaMakefile
src/HOL/Makefile
     1.1 --- a/src/HOL/IsaMakefile	Wed Apr 30 11:56:17 1997 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Apr 30 11:58:23 1997 +0200
     1.3 @@ -71,24 +71,14 @@
     1.4  	@$(ISATOOL) usedir $(OUT)/HOL Integ
     1.5  
     1.6  
     1.7 -## I/O Automata
     1.8 +## I/O Automata (meta theory only)
     1.9  
    1.10 -IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet \
    1.11 -		Receiver Sender
    1.12 -IOA_ABP_NAMES = Action Correctness Lemmas
    1.13 -IOA_MT_NAMES = Asig IOA Solve
    1.14  
    1.15 -IOA_FILES = IOA/NTP/ROOT.ML IOA/ABP/ROOT.ML IOA/NTP/Spec.thy \
    1.16 - $(IOA_NTP_NAMES:%=IOA/NTP/%.thy) $(IOA_NTP_NAMES:%=IOA/NTP/%.ML) \
    1.17 - IOA/ABP/Abschannel.thy IOA/ABP/Abschannel_finite.thy IOA/ABP/Env.thy \
    1.18 - IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy IOA/ABP/Packet.thy \
    1.19 - IOA/ABP/Receiver.thy IOA/ABP/Sender.thy IOA/ABP/Spec.thy \
    1.20 - $(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML) \
    1.21 - $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
    1.22 +IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \
    1.23 +  IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML
    1.24  
    1.25 -IOA:	$(OUT)/HOL $(IOA_FILES)
    1.26 -	@$(ISATOOL) usedir -s IOA-NTP $(OUT)/HOL IOA/NTP
    1.27 -	@$(ISATOOL) usedir -s IOA-ABP $(OUT)/HOL IOA/ABP
    1.28 +IOA: $(OUT)/HOL $(IOA_FILES)
    1.29 +	@$(ISATOOL) usedir $(OUT)/HOL IOA
    1.30  
    1.31  
    1.32  ## Authentication & Security Protocols
     2.1 --- a/src/HOL/Makefile	Wed Apr 30 11:56:17 1997 +0200
     2.2 +++ b/src/HOL/Makefile	Wed Apr 30 11:58:23 1997 +0200
     2.3 @@ -121,30 +121,6 @@
     2.4  	else echo 'exit_use_dir"Integ";quit();' | $(LOGIC); \
     2.5  	fi
     2.6  
     2.7 -##I/O Automata
     2.8 -IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet\
     2.9 -		Receiver Sender
    2.10 -IOA_ABP_NAMES = Action Correctness Lemmas
    2.11 -IOA_MT_NAMES = Asig IOA Solve
    2.12 -
    2.13 -IOA_FILES = IOA/NTP/ROOT.ML IOA/ABP/ROOT.ML IOA/NTP/Spec.thy\
    2.14 - $(IOA_NTP_NAMES:%=IOA/NTP/%.thy) $(IOA_NTP_NAMES:%=IOA/NTP/%.ML)\
    2.15 - IOA/ABP/Abschannel.thy IOA/ABP/Abschannel_finite.thy IOA/ABP/Env.thy\
    2.16 - IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy IOA/ABP/Packet.thy\
    2.17 - IOA/ABP/Receiver.thy IOA/ABP/Sender.thy IOA/ABP/Spec.thy\
    2.18 - $(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML)\
    2.19 - $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
    2.20 -
    2.21 -IOA:	$(BIN)/HOL  $(IOA_FILES)
    2.22 -	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    2.23 -	then echo 'make_html := true; exit_use_dir"IOA/NTP";quit();' \
    2.24 -	       | $(LOGIC);\
    2.25 -	     echo 'make_html := true; exit_use_dir"IOA/ABP";quit();' \
    2.26 -	       | $(LOGIC);\
    2.27 -	else echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC); \
    2.28 -	     echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC); \
    2.29 -	fi
    2.30 -
    2.31  
    2.32  ##Authentication & Security Protocols
    2.33  Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
    2.34 @@ -238,7 +214,7 @@
    2.35  	fi
    2.36  
    2.37  #Full test.
    2.38 -test:	$(BIN)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
    2.39 +test:	$(BIN)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda MiniML ex
    2.40  	echo 'Test examples ran successfully' > test
    2.41  
    2.42  .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL