equal
deleted
inserted
replaced
26 wf.thy wf.ML ord.thy ord.ML nat.thy nat.ML \ |
26 wf.thy wf.ML ord.thy ord.ML nat.thy nat.ML \ |
27 epsilon.thy epsilon.ML arith.thy arith.ML univ.thy univ.ML \ |
27 epsilon.thy epsilon.ML arith.thy arith.ML univ.thy univ.ML \ |
28 quniv.thy quniv.ML constructor.ML datatype.ML \ |
28 quniv.thy quniv.ML constructor.ML datatype.ML \ |
29 fin.ML list.ML listfn.thy listfn.ML |
29 fin.ML list.ML listfn.thy listfn.ML |
30 |
30 |
|
31 EX_FILES = ex/ROOT.ML ex/acc.ML ex/bin.ML ex/binfn.ML ex/binfn.thy\ |
|
32 ex/bt.ML ex/bt_fn.ML ex/bt_fn.thy ex/comb.ML\ |
|
33 ex/contract0.ML ex/contract0.thy ex/counit.ML ex/data.ML\ |
|
34 ex/enum.ML ex/equiv.ML ex/equiv.thy ex/integ.ML ex/integ.thy\ |
|
35 ex/listn.ML ex/llist.ML ex/llist_eq.ML ex/llistfn.ML ex/llistfn.thy\ |
|
36 ex/misc.ML ex/parcontract.ML ex/primrec0.ML ex/primrec0.thy\ |
|
37 ex/prop.ML ex/proplog.ML ex/proplog.thy ex/ramsey.ML ex/ramsey.thy\ |
|
38 ex/rmap.ML ex/term.ML ex/termfn.ML ex/termfn.thy ex/tf.ML\ |
|
39 ex/tf_fn.ML ex/tf_fn.thy ex/twos_compl.ML |
|
40 |
31 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
41 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
32 $(BIN)/ZF: $(BIN)/FOL $(FILES) |
42 $(BIN)/ZF: $(BIN)/FOL $(FILES) |
33 case "$(COMP)" in \ |
43 case "$(COMP)" in \ |
34 poly*) cp $(BIN)/FOL $(BIN)/ZF;\ |
44 poly*) cp $(BIN)/FOL $(BIN)/ZF;\ |
35 echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\ |
45 echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/ZF ;;\ |
38 esac |
48 esac |
39 |
49 |
40 $(BIN)/FOL: |
50 $(BIN)/FOL: |
41 cd ../FOL; $(MAKE) |
51 cd ../FOL; $(MAKE) |
42 |
52 |
43 test: ex/ROOT.ML $(BIN)/ZF |
53 test: ex/ROOT.ML $(BIN)/ZF $(EX_FILES) |
44 case "$(COMP)" in \ |
54 case "$(COMP)" in \ |
45 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/ZF ;;\ |
55 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/ZF ;;\ |
46 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/ZF;;\ |
56 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/ZF;;\ |
47 *) echo Bad value for ISABELLECOMP;;\ |
57 *) echo Bad value for ISABELLECOMP;;\ |
48 esac |
58 esac |