src/HOL/Makefile
changeset 944 01d6571fa106
parent 923 ff1574a81019
child 953 17d7fad9c9a2
equal deleted inserted replaced
943:8477483f663f 944:01d6571fa106
    24        Finite.thy Arith.thy Sexp.thy Univ.thy List.thy 
    24        Finite.thy Arith.thy Sexp.thy Univ.thy List.thy 
    25 
    25 
    26 FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\
    26 FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\
    27 	ind_syntax.ML indrule.ML intr_elim.ML simpdata.ML\
    27 	ind_syntax.ML indrule.ML intr_elim.ML simpdata.ML\
    28 	subtype.ML thy_syntax.ML ../Pure/section_utils.ML\
    28 	subtype.ML thy_syntax.ML ../Pure/section_utils.ML\
    29 	../Provers/classical.ML ../Provers/simplifier.ML \
    29 	../Provers/hypsubst.ML ../Provers/classical.ML\
    30 	../Provers/splitter.ML ../Provers/ind.ML $(THYS) $(THYS:.thy=.ML)
    30         ../Provers/simplifier.ML ../Provers/splitter.ML\
       
    31         $(THYS) $(THYS:.thy=.ML)
    31 
    32 
    32 $(BIN)/CHOL:   $(BIN)/Pure  $(FILES) 
    33 $(BIN)/CHOL:   $(BIN)/Pure  $(FILES) 
    33 	if [ -d $${ISABELLEBIN:?}/Pure ];\
    34 	if [ -d $${ISABELLEBIN:?}/Pure ];\
    34            	then echo Bad value for ISABELLEBIN: \
    35            	then echo Bad value for ISABELLEBIN: \
    35                 	$(BIN) is the Isabelle source directory; \
    36                 	$(BIN) is the Isabelle source directory; \