equal
deleted
inserted
replaced
223 then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\ |
223 then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\ |
224 else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \ |
224 else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \ |
225 fi |
225 fi |
226 |
226 |
227 ##Miscellaneous examples |
227 ##Miscellaneous examples |
228 EX_NAMES = String BT Perm Comb InSort Qsort LexProd \ |
228 EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \ |
229 Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT |
229 Primes NatSum SList LList LFilter Acc PropLog Term Simult MT |
230 |
230 |
231 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ |
231 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ |
232 ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
232 ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
233 |
233 |
234 ex: $(BIN)/HOL $(EX_FILES) |
234 ex: $(BIN)/HOL $(EX_FILES) |