src/HOL/Makefile
changeset 1044 5bf29088250e
parent 953 17d7fad9c9a2
child 1063 d33e3523a5e6
     1.1 --- a/src/HOL/Makefile	Thu Apr 13 14:25:45 1995 +0200
     1.2 +++ b/src/HOL/Makefile	Thu Apr 13 15:03:07 1995 +0200
     1.3 @@ -18,17 +18,15 @@
     1.4  
     1.5  BIN = $(ISABELLEBIN)
     1.6  COMP = $(ISABELLECOMP)
     1.7 -THYS = HOL.thy Ord.thy Set.thy Fun.thy subset.thy \
     1.8 -       equalities.thy Prod.thy Trancl.thy Sum.thy WF.thy \
     1.9 -       mono.thy Lfp.thy Gfp.thy Nat.thy Inductive.thy \
    1.10 -       Finite.thy Arith.thy Sexp.thy Univ.thy List.thy 
    1.11 +NAMES = HOL Ord Set Fun subset equalities Prod Trancl Sum WF \
    1.12 +       mono Lfp Gfp Nat Inductive Finite Arith Sexp Univ List 
    1.13  
    1.14  FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\
    1.15  	ind_syntax.ML indrule.ML intr_elim.ML simpdata.ML\
    1.16  	subtype.ML thy_syntax.ML ../Pure/section_utils.ML\
    1.17  	../Provers/hypsubst.ML ../Provers/classical.ML\
    1.18          ../Provers/simplifier.ML ../Provers/splitter.ML\
    1.19 -        $(THYS) $(THYS:.thy=.ML)
    1.20 + 	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    1.21  
    1.22  $(BIN)/CHOL:   $(BIN)/Pure  $(FILES) 
    1.23  	if [ -d $${ISABELLEBIN:?}/Pure ];\
    1.24 @@ -59,51 +57,46 @@
    1.25  	esac
    1.26  
    1.27  ##IMP-semantics example
    1.28 -IMP_THYS = IMP/Com.thy IMP/Denotation.thy IMP/Equiv.thy IMP/Properties.thy
    1.29 -IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
    1.30 +IMP_NAMES = Com Denotation Equiv Properties
    1.31 +IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    1.32  
    1.33  IMP:    $(BIN)/CHOL  $(IMP_FILES)
    1.34  	echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
    1.35  
    1.36  ##The integers in CHOL
    1.37 -INTEG_THYS = Integ/Relation.thy Integ/Equiv.thy Integ/Integ.thy 
    1.38 +INTEG_NAMES = Relation Equiv Integ 
    1.39  
    1.40 -INTEG_FILES = Integ/ROOT.ML $(INTEG_THYS) $(INTEG_THYS:.thy=.ML)
    1.41 +INTEG_FILES = Integ/ROOT.ML \
    1.42 +              $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
    1.43  
    1.44  Integ:  $(BIN)/CHOL  $(INTEG_FILES)
    1.45  	echo 'exit_use"Integ/ROOT.ML";quit();' | $(LOGIC)
    1.46  
    1.47  ##I/O Automata
    1.48 -IOA_THYS = IOA/example/Action.thy IOA/example/Channels.thy\
    1.49 -	   IOA/example/Correctness.thy IOA/example/Impl.thy \
    1.50 -	   IOA/example/Lemmas.thy IOA/example/Multiset.thy \
    1.51 -	   IOA/example/Receiver.thy IOA/example/Sender.thy \
    1.52 -	   IOA/meta_theory/Asig.thy IOA/meta_theory/IOA.thy \
    1.53 -	   IOA/meta_theory/Option.thy IOA/meta_theory/Solve.thy
    1.54 +IOA_EX_NAMES = Action Channels Correctness Impl Lemmas Multiset Receiver Sender
    1.55 +IOA_MT_NAMES = Asig IOA Option Solve
    1.56  
    1.57  IOA_FILES = IOA/ROOT.ML IOA/example/Packet.thy IOA/example/Spec.thy\
    1.58 -	    $(IOA_THYS) $(IOA_THYS:.thy=.ML)
    1.59 + $(IOA_EX_NAMES:%=IOA/example/%.thy) $(IOA_EX_NAMES:%=IOA/example/%.ML)\
    1.60 + $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
    1.61  
    1.62  IOA:    $(BIN)/CHOL  $(IOA_FILES)
    1.63  	echo 'exit_use"IOA/ROOT.ML";quit();' | $(LOGIC)
    1.64  
    1.65  ##Properties of substitutions
    1.66 -SUBST_THYS = Subst/AList.thy Subst/Setplus.thy\
    1.67 -	     Subst/Subst.thy Subst/Unifier.thy\
    1.68 -	     Subst/UTerm.thy Subst/UTLemmas.thy
    1.69 +SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
    1.70  
    1.71 -SUBST_FILES = Subst/ROOT.ML $(SUBST_THYS) $(SUBST_THYS:.thy=.ML)
    1.72 +SUBST_FILES = Subst/ROOT.ML \
    1.73 +              $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
    1.74  
    1.75  Subst:  $(BIN)/CHOL  $(SUBST_FILES)
    1.76  	echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC)
    1.77  
    1.78  ##Miscellaneous examples
    1.79 -EX_THYS = ex/LexProd.thy ex/MT.thy ex/Acc.thy \
    1.80 -	  ex/PropLog.thy ex/Puzzle.thy ex/Qsort.thy ex/LList.thy \
    1.81 -	  ex/Rec.thy ex/Simult.thy ex/Term.thy ex/String.thy 
    1.82 +EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String 
    1.83  
    1.84  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
    1.85 -           ex/set.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
    1.86 +           ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
    1.87  
    1.88  ex:     $(BIN)/CHOL  $(EX_FILES)
    1.89  	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)