equal
deleted
inserted
replaced
86 $(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML)\ |
86 $(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML)\ |
87 $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML) |
87 $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML) |
88 |
88 |
89 IOA: $(BIN)/HOL $(IOA_FILES) |
89 IOA: $(BIN)/HOL $(IOA_FILES) |
90 echo 'exit_use"IOA/ROOT_NTP.ML";quit();' | $(LOGIC) |
90 echo 'exit_use"IOA/ROOT_NTP.ML";quit();' | $(LOGIC) |
91 echo 'exit_use"IOA/ROOT_ABP.ML";quit();' | $(LOGIC) |
91 # echo 'exit_use"IOA/ROOT_ABP.ML";quit();' | $(LOGIC) |
92 |
92 |
93 ##Properties of substitutions |
93 ##Properties of substitutions |
94 SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas |
94 SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas |
95 |
95 |
96 SUBST_FILES = Subst/ROOT.ML \ |
96 SUBST_FILES = Subst/ROOT.ML \ |
116 ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
116 ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
117 |
117 |
118 ex: $(BIN)/HOL $(EX_FILES) |
118 ex: $(BIN)/HOL $(EX_FILES) |
119 echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC) |
119 echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC) |
120 |
120 |
121 #Full test. |
121 #Full test. (IOA has been removed temporarily) |
122 test: $(BIN)/HOL IMP Integ IOA Subst Lambda ex |
122 test: $(BIN)/HOL IMP Integ Subst Lambda ex |
123 echo 'Test examples ran successfully' > test |
123 echo 'Test examples ran successfully' > test |
124 |
124 |
125 .PRECIOUS: $(BIN)/Pure $(BIN)/HOL |
125 .PRECIOUS: $(BIN)/Pure $(BIN)/HOL |