# HG changeset patch
# User clasohm
# Date 816954112 -3600
# Node ID 5bf4a54ba25f215cc792fe03f987c7c85c58b729
# Parent  ef26adb4e5b67c62b1e9fee74de8886797b9bac9
replaced exit_use by exit_use_dir for subdirectories

diff -r ef26adb4e5b6 -r 5bf4a54ba25f src/CCL/Makefile
--- a/src/CCL/Makefile	Tue Nov 21 12:40:04 1995 +0100
+++ b/src/CCL/Makefile	Tue Nov 21 12:41:52 1995 +0100
@@ -55,8 +55,9 @@
 
 test:   ex/ROOT.ML  $(BIN)/CCL  $(EX_FILES)
 	case "$(COMP)" in \
-	poly*)	echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CCL ;;\
-	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CCL;;\
+	poly*)	echo 'exit_use_dir"ex"; quit();' \
+                  | $(COMP) $(BIN)/CCL ;;\
+	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/CCL;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r ef26adb4e5b6 -r 5bf4a54ba25f src/FOL/Makefile
--- a/src/FOL/Makefile	Tue Nov 21 12:40:04 1995 +0100
+++ b/src/FOL/Makefile	Tue Nov 21 12:41:52 1995 +0100
@@ -58,8 +58,8 @@
 
 test:   ex/ROOT.ML  $(BIN)/FOL  $(EX_FILES) 
 	case "$(COMP)" in \
-	poly*)	echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOL ;;\
-	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/FOL;;\
+	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL ;;\
+	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/FOL;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r ef26adb4e5b6 -r 5bf4a54ba25f src/FOLP/Makefile
--- a/src/FOLP/Makefile	Tue Nov 21 12:40:04 1995 +0100
+++ b/src/FOLP/Makefile	Tue Nov 21 12:41:52 1995 +0100
@@ -52,8 +52,8 @@
 
 test:   ex/ROOT.ML  $(BIN)/FOLP  $(EX_FILES) 
 	case "$(COMP)" in \
-	poly*)	echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOLP ;;\
-	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/FOLP;;\
+	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP ;;\
+	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/FOLP;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r ef26adb4e5b6 -r 5bf4a54ba25f src/HOL/Makefile
--- a/src/HOL/Makefile	Tue Nov 21 12:40:04 1995 +0100
+++ b/src/HOL/Makefile	Tue Nov 21 12:41:52 1995 +0100
@@ -72,14 +72,14 @@
 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
 
 IMP:    $(BIN)/HOL  $(IMP_FILES)
-	echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use_dir"IMP";quit();' | $(LOGIC)
 
 ##Hoare logic
 Hoare_NAMES = Hoare Arith2 Examples
 Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) $(Hoare_NAMES:%=Hoare/%.ML)
 
 Hoare:  $(BIN)/HOL  $(Hoare_FILES)
-	echo 'exit_use"Hoare/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use_dir"Hoare";quit();' | $(LOGIC)
 
 ##The integers in HOL
 INTEG_NAMES = Equiv Integ 
@@ -88,7 +88,7 @@
               $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
 
 Integ:  $(BIN)/HOL  $(INTEG_FILES)
-	echo 'exit_use"Integ/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use_dir"Integ";quit();' | $(LOGIC)
 
 ##I/O Automata
 IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet\
@@ -96,7 +96,7 @@
 IOA_ABP_NAMES = Action Correctness Lemmas
 IOA_MT_NAMES = Asig IOA Option Solve
 
-IOA_FILES = IOA/ROOT_NTP.ML IOA/ROOT_ABP.ML IOA/NTP/Spec.thy\
+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\
@@ -105,8 +105,8 @@
  $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
 
 IOA:    $(BIN)/HOL  $(IOA_FILES)
-	echo 'exit_use"IOA/ROOT_NTP.ML";quit();' | $(LOGIC)
-#	echo 'exit_use"IOA/ROOT_ABP.ML";quit();' | $(LOGIC)
+	echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC)
+	echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC)
 
 ##Properties of substitutions
 SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
@@ -115,7 +115,7 @@
               $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
 
 Subst:  $(BIN)/HOL  $(SUBST_FILES)
-	echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use_dir"Subst";quit();' | $(LOGIC)
 
 ##Confluence of Lambda-calculus
 LAMBDA_NAMES = Lambda ParRed Commutation Eta
@@ -123,8 +123,8 @@
 LAMBDA_FILES = Lambda/ROOT.ML \
               $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
 
-Lambda:	$(BIN)/HOL  $(LAMBDA_FILES)
-	echo 'exit_use"Lambda/ROOT.ML";quit();' | $(LOGIC)
+Lambda:  $(BIN)/HOL $(LAMBDA_FILES)
+	echo 'exit_use_dir"Lambda";quit();' | $(LOGIC)
 
 ##Type inference for MiniML
 MINIML_NAMES = I Maybe MiniML Type W
@@ -132,8 +132,8 @@
 MINIML_FILES = MiniML/ROOT.ML \
               $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
 
-MiniML:	$(BIN)/HOL  $(MINIML_FILES)
-	echo 'exit_use"MiniML/ROOT.ML";quit();' | $(LOGIC)
+MiniML: $(BIN)/HOL  $(MINIML_FILES)
+	echo 'exit_use_dir"MiniML";quit();' | $(LOGIC)
 
 ##Lexical analysis
 LEX_FILES = Auto AutoChopper Chopper Prefix
@@ -142,7 +142,7 @@
             $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
 
 Lex:	$(BIN)/HOL  $(LEX_FILES)
-	echo 'exit_use"Lex/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use_dir"Lex";quit();' | $(LOGIC)
 
 ##Miscellaneous examples
 EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String \
@@ -152,7 +152,7 @@
            ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
 
 ex:     $(BIN)/HOL  $(EX_FILES)
-	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use_dir"ex";quit();' | $(LOGIC)
 
 #Full test.
 test:   $(BIN)/HOL IMP Hoare Lex Integ Subst Lambda MiniML IOA ex
diff -r ef26adb4e5b6 -r 5bf4a54ba25f src/HOLCF/Makefile
--- a/src/HOLCF/Makefile	Tue Nov 21 12:40:04 1995 +0100
+++ b/src/HOLCF/Makefile	Tue Nov 21 12:41:52 1995 +0100
@@ -61,8 +61,8 @@
 
 test:   ex/ROOT.ML  $(BIN)/HOLCF  $(EX_FILES) 
 	case "$(COMP)" in \
-	poly*)	echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/HOLCF ;;\
-	sml*)	echo 'exit_use"ex/ROOT.ML"' | $(BIN)/HOLCF;;\
+	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/HOLCF ;;\
+	sml*)	echo 'exit_use_dir"ex"' | $(BIN)/HOLCF;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
@@ -77,8 +77,9 @@
 
 test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF  $(EXPLICIT_DOMAINS_FILES) 
 	case "$(COMP)" in \
-	poly*)	echo 'exit_use"explicit_domains/ROOT.ML"; quit();' | $(COMP) $(BIN)/HOLCF ;;\
-	sml*)	echo 'exit_use"explicit_domains/ROOT.ML"' | $(BIN)/HOLCF;;\
+	poly*)	echo 'exit_use_dir"explicit_domains"; quit();' \
+                  | $(COMP) $(BIN)/HOLCF ;;\
+	sml*)	echo 'exit_use_dir"explicit_domains"' | $(BIN)/HOLCF;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r ef26adb4e5b6 -r 5bf4a54ba25f src/ZF/Makefile
--- a/src/ZF/Makefile	Tue Nov 21 12:40:04 1995 +0100
+++ b/src/ZF/Makefile	Tue Nov 21 12:41:52 1995 +0100
@@ -69,7 +69,7 @@
 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
 
 IMP:   $(BIN)/ZF  $(IMP_FILES)
-	echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use_dir"IMP";quit();' | $(LOGIC)
 
 ##Coinduction example
 COIND_NAMES = ECR Language MT Map Static Types Values 
@@ -78,7 +78,7 @@
               $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
 
 Coind:  $(BIN)/ZF  $(COIND_FILES)
-	echo 'exit_use"Coind/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use_dir"Coind";quit();' | $(LOGIC)
 
 ##AC examples
 AC_NAMES = AC_Equiv OrdQuant Transrec2 Cardinal_aux \
@@ -92,7 +92,7 @@
            $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
 
 AC:  $(BIN)/ZF  $(AC_FILES)
-	echo 'exit_use"AC/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use_dir"AC";quit();' | $(LOGIC)
 
 ##Residuals example
 
@@ -103,7 +103,7 @@
                             $(RESID_NAMES:%=Resid/%.ML)
 
 Resid:  $(BIN)/ZF  $(RESID_FILES)
-	echo 'exit_use"Resid/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use_dir"Resid";quit();' | $(LOGIC)
 
 ##Miscellaneous examples
 EX_NAMES = Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
@@ -113,7 +113,7 @@
 
 #Test ZF by loading the examples in directory ex
 ex:     $(BIN)/ZF  $(EX_FILES)
-	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use_dir"ex";quit();' | $(LOGIC)
 
 #Full test.
 test:   $(BIN)/ZF IMP Coind AC Resid ex