equal
deleted
inserted
replaced
270 |
270 |
271 |
271 |
272 ## HOL-Complex-Import |
272 ## HOL-Complex-Import |
273 |
273 |
274 IMPORTER_FILES = Import/lazy_seq.ML Import/proof_kernel.ML Import/replay.ML \ |
274 IMPORTER_FILES = Import/lazy_seq.ML Import/proof_kernel.ML Import/replay.ML \ |
275 Import/susp.ML Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \ |
275 Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \ |
276 Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \ |
276 Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \ |
277 Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML |
277 Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML |
278 |
278 |
279 IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \ |
279 IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \ |
280 Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \ |
280 Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \ |