author | wenzelm |
Sat, 08 Oct 2005 22:39:39 +0200 | |
changeset 17801 | 30cbd2685e73 |
parent 17800 | d39171dda84e |
child 17802 | f3b1ca16cebd |
--- a/src/HOL/Import/HOL4Setup.thy Sat Oct 08 22:39:38 2005 +0200 +++ b/src/HOL/Import/HOL4Setup.thy Sat Oct 08 22:39:39 2005 +0200 @@ -4,7 +4,8 @@ *) theory HOL4Setup imports MakeEqual - uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin + uses "susp.ML" "lazy_seq.ML" "lazy_scan.ML" + ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin section {* General Setup *}