src/HOL/Makefile
changeset 1350 5bf4a54ba25f
parent 1343 8770c062b092
child 1357 dac9989eb88f
     1.1 --- a/src/HOL/Makefile	Tue Nov 21 12:40:04 1995 +0100
     1.2 +++ b/src/HOL/Makefile	Tue Nov 21 12:41:52 1995 +0100
     1.3 @@ -72,14 +72,14 @@
     1.4  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
     1.5  
     1.6  IMP:    $(BIN)/HOL  $(IMP_FILES)
     1.7 -	echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
     1.8 +	echo 'exit_use_dir"IMP";quit();' | $(LOGIC)
     1.9  
    1.10  ##Hoare logic
    1.11  Hoare_NAMES = Hoare Arith2 Examples
    1.12  Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) $(Hoare_NAMES:%=Hoare/%.ML)
    1.13  
    1.14  Hoare:  $(BIN)/HOL  $(Hoare_FILES)
    1.15 -	echo 'exit_use"Hoare/ROOT.ML";quit();' | $(LOGIC)
    1.16 +	echo 'exit_use_dir"Hoare";quit();' | $(LOGIC)
    1.17  
    1.18  ##The integers in HOL
    1.19  INTEG_NAMES = Equiv Integ 
    1.20 @@ -88,7 +88,7 @@
    1.21                $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
    1.22  
    1.23  Integ:  $(BIN)/HOL  $(INTEG_FILES)
    1.24 -	echo 'exit_use"Integ/ROOT.ML";quit();' | $(LOGIC)
    1.25 +	echo 'exit_use_dir"Integ";quit();' | $(LOGIC)
    1.26  
    1.27  ##I/O Automata
    1.28  IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet\
    1.29 @@ -96,7 +96,7 @@
    1.30  IOA_ABP_NAMES = Action Correctness Lemmas
    1.31  IOA_MT_NAMES = Asig IOA Option Solve
    1.32  
    1.33 -IOA_FILES = IOA/ROOT_NTP.ML IOA/ROOT_ABP.ML IOA/NTP/Spec.thy\
    1.34 +IOA_FILES = IOA/NTP/ROOT.ML IOA/ABP/ROOT.ML IOA/NTP/Spec.thy\
    1.35   $(IOA_NTP_NAMES:%=IOA/NTP/%.thy) $(IOA_NTP_NAMES:%=IOA/NTP/%.ML)\
    1.36   IOA/ABP/Abschannel.thy IOA/ABP/Abschannel_finite.thy IOA/ABP/Env.thy\
    1.37   IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy IOA/ABP/Packet.thy\
    1.38 @@ -105,8 +105,8 @@
    1.39   $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
    1.40  
    1.41  IOA:    $(BIN)/HOL  $(IOA_FILES)
    1.42 -	echo 'exit_use"IOA/ROOT_NTP.ML";quit();' | $(LOGIC)
    1.43 -#	echo 'exit_use"IOA/ROOT_ABP.ML";quit();' | $(LOGIC)
    1.44 +	echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC)
    1.45 +	echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC)
    1.46  
    1.47  ##Properties of substitutions
    1.48  SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
    1.49 @@ -115,7 +115,7 @@
    1.50                $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
    1.51  
    1.52  Subst:  $(BIN)/HOL  $(SUBST_FILES)
    1.53 -	echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC)
    1.54 +	echo 'exit_use_dir"Subst";quit();' | $(LOGIC)
    1.55  
    1.56  ##Confluence of Lambda-calculus
    1.57  LAMBDA_NAMES = Lambda ParRed Commutation Eta
    1.58 @@ -123,8 +123,8 @@
    1.59  LAMBDA_FILES = Lambda/ROOT.ML \
    1.60                $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
    1.61  
    1.62 -Lambda:	$(BIN)/HOL  $(LAMBDA_FILES)
    1.63 -	echo 'exit_use"Lambda/ROOT.ML";quit();' | $(LOGIC)
    1.64 +Lambda:  $(BIN)/HOL $(LAMBDA_FILES)
    1.65 +	echo 'exit_use_dir"Lambda";quit();' | $(LOGIC)
    1.66  
    1.67  ##Type inference for MiniML
    1.68  MINIML_NAMES = I Maybe MiniML Type W
    1.69 @@ -132,8 +132,8 @@
    1.70  MINIML_FILES = MiniML/ROOT.ML \
    1.71                $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
    1.72  
    1.73 -MiniML:	$(BIN)/HOL  $(MINIML_FILES)
    1.74 -	echo 'exit_use"MiniML/ROOT.ML";quit();' | $(LOGIC)
    1.75 +MiniML: $(BIN)/HOL  $(MINIML_FILES)
    1.76 +	echo 'exit_use_dir"MiniML";quit();' | $(LOGIC)
    1.77  
    1.78  ##Lexical analysis
    1.79  LEX_FILES = Auto AutoChopper Chopper Prefix
    1.80 @@ -142,7 +142,7 @@
    1.81              $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
    1.82  
    1.83  Lex:	$(BIN)/HOL  $(LEX_FILES)
    1.84 -	echo 'exit_use"Lex/ROOT.ML";quit();' | $(LOGIC)
    1.85 +	echo 'exit_use_dir"Lex";quit();' | $(LOGIC)
    1.86  
    1.87  ##Miscellaneous examples
    1.88  EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String \
    1.89 @@ -152,7 +152,7 @@
    1.90             ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
    1.91  
    1.92  ex:     $(BIN)/HOL  $(EX_FILES)
    1.93 -	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
    1.94 +	echo 'exit_use_dir"ex";quit();' | $(LOGIC)
    1.95  
    1.96  #Full test.
    1.97  test:   $(BIN)/HOL IMP Hoare Lex Integ Subst Lambda MiniML IOA ex