equal
deleted
inserted
replaced
242 @$(ISATOOL) usedir $(OUT)/HOL IMPP |
242 @$(ISATOOL) usedir $(OUT)/HOL IMPP |
243 |
243 |
244 |
244 |
245 ## HOL-Complex-Import |
245 ## HOL-Complex-Import |
246 |
246 |
247 IMPORTER_FILES = Import/proof_kernel.ML Import/replay.ML \ |
247 IMPORTER_FILES = Import/lazy_seq.ML Import/lazy_scan.ML \ |
|
248 Import/proof_kernel.ML Import/replay.ML Import/susp.ML \ |
248 Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \ |
249 Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \ |
249 Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \ |
250 Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \ |
250 Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML |
251 Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML |
251 |
252 |
252 IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \ |
253 IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \ |