equal
deleted
inserted
replaced
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; \ |