96 $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML) |
96 $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML) |
97 |
97 |
98 Subst: $(BIN)/CHOL $(SUBST_FILES) |
98 Subst: $(BIN)/CHOL $(SUBST_FILES) |
99 echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC) |
99 echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC) |
100 |
100 |
|
101 ##Confluence of Lambda-calculus |
|
102 LAMBDA_NAMES = Lambda ParRed Confluence |
|
103 |
|
104 LAMBDA_FILES = Lambda/ROOT.ML \ |
|
105 $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML) |
|
106 |
|
107 Lambda: $(BIN)/CHOL $(LAMBDA_FILES) |
|
108 echo 'exit_use"Lambda/ROOT.ML";quit();' | $(LOGIC) |
|
109 |
101 ##Miscellaneous examples |
110 ##Miscellaneous examples |
102 EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String |
111 EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String |
103 |
112 |
104 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ |
113 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ |
105 ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
114 ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
106 |
115 |
107 ex: $(BIN)/CHOL $(EX_FILES) |
116 ex: $(BIN)/CHOL $(EX_FILES) |
108 echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC) |
117 echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC) |
109 |
118 |
110 #Full test. |
119 #Full test. |
111 test: $(BIN)/CHOL IMP Integ IOA Subst ex |
120 test: $(BIN)/CHOL IMP Integ IOA Subst Lambda ex |
112 echo 'Test examples ran successfully' > test |
121 echo 'Test examples ran successfully' > test |
113 |
122 |
114 .PRECIOUS: $(BIN)/Pure $(BIN)/CHOL |
123 .PRECIOUS: $(BIN)/Pure $(BIN)/CHOL |