equal
deleted
inserted
replaced
198 @$(ISATOOL) usedir $(OUT)/HOL Quot |
198 @$(ISATOOL) usedir $(OUT)/HOL Quot |
199 |
199 |
200 |
200 |
201 ## Miscellaneous examples |
201 ## Miscellaneous examples |
202 |
202 |
203 EX_NAMES = Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT |
203 EX_NAMES = Recdef Fib Primes Primrec NatSum String BT InSort Qsort Puzzle MT |
204 |
204 |
205 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ |
205 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \ |
206 ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
206 ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML) |
207 |
207 |
208 ex: $(OUT)/HOL $(EX_FILES) |
208 ex: $(OUT)/HOL $(EX_FILES) |