25 ex/intro.ML ex/List.ML ex/List.thy ex/Nat.ML ex/Nat.thy\ |
25 ex/intro.ML ex/List.ML ex/List.thy ex/Nat.ML ex/Nat.thy\ |
26 ex/Nat2.ML ex/Nat2.thy ex/Prolog.ML ex/Prolog.thy ex/prop.ML\ |
26 ex/Nat2.ML ex/Nat2.thy ex/Prolog.ML ex/Prolog.thy ex/prop.ML\ |
27 ex/quant.ML |
27 ex/quant.ML |
28 |
28 |
29 $(BIN)/FOL: $(BIN)/Pure $(FILES) |
29 $(BIN)/FOL: $(BIN)/Pure $(FILES) |
|
30 if [ -d $${ISABELLEBIN:?}/Pure ];\ |
|
31 then echo Bad value for ISABELLEBIN: \ |
|
32 $(BIN) is the Isabelle source directory; \ |
|
33 exit 1; \ |
|
34 fi;\ |
30 case "$(COMP)" in \ |
35 case "$(COMP)" in \ |
31 poly*) echo 'make_database"$(BIN)/FOL"; quit();' \ |
36 poly*) echo 'make_database"$(BIN)/FOL"; quit();' \ |
32 | $(COMP) $(BIN)/Pure;\ |
37 | $(COMP) $(BIN)/Pure;\ |
33 echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/FOL;;\ |
38 echo 'open PolyML; use"ROOT";' | $(COMP) $(BIN)/FOL;;\ |
34 sml*) echo 'use"ROOT.ML"; xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;;\ |
39 sml*) echo 'use"ROOT.ML"; xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;;\ |
35 *) echo Bad value for ISABELLECOMP;;\ |
40 *) echo Bad value for ISABELLECOMP: \ |
|
41 $(COMP) is not poly or sml;;\ |
36 esac |
42 esac |
37 |
43 |
38 $(BIN)/Pure: |
44 $(BIN)/Pure: |
39 cd ../Pure; $(MAKE) |
45 cd ../Pure; $(MAKE) |
40 |
46 |
41 test: ex/ROOT.ML $(BIN)/FOL $(EX_FILES) |
47 test: ex/ROOT.ML $(BIN)/FOL $(EX_FILES) |
42 case "$(COMP)" in \ |
48 case "$(COMP)" in \ |
43 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOL ;;\ |
49 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOL ;;\ |
44 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/FOL;;\ |
50 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/FOL;;\ |
45 *) echo Bad value for ISABELLECOMP;;\ |
51 *) echo Bad value for ISABELLECOMP: \ |
|
52 $(COMP) is not poly or sml;;\ |
46 esac |
53 esac |
47 |
54 |
48 .PRECIOUS: $(BIN)/Pure $(BIN)/FOL |
55 .PRECIOUS: $(BIN)/Pure $(BIN)/FOL |