equal
deleted
inserted
replaced
28 FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\ |
28 FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\ |
29 ind_syntax.ML cladata.ML simpdata.ML\ |
29 ind_syntax.ML cladata.ML simpdata.ML\ |
30 typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML\ |
30 typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML\ |
31 ../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \ |
31 ../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \ |
32 ../Provers/simplifier.ML ../Provers/splitter.ML\ |
32 ../Provers/simplifier.ML ../Provers/splitter.ML\ |
|
33 ../Provers/nat_transitive.ML \ |
33 $(NAMES:%=%.thy) $(NAMES:%=%.ML) |
34 $(NAMES:%=%.thy) $(NAMES:%=%.ML) |
34 |
35 |
35 $(BIN)/HOL: $(BIN)/Pure $(FILES) |
36 $(BIN)/HOL: $(BIN)/Pure $(FILES) |
36 @if [ -d $${ISABELLEBIN:?}/Pure ];\ |
37 @if [ -d $${ISABELLEBIN:?}/Pure ];\ |
37 then echo Bad value for ISABELLEBIN: \ |
38 then echo Bad value for ISABELLEBIN: \ |