uses susp.ML, lazy_seq.ML, lazy_scan.ML;
authorwenzelm
Sat, 08 Oct 2005 22:39:39 +0200
changeset 17801 30cbd2685e73
parent 17800 d39171dda84e
child 17802 f3b1ca16cebd
uses susp.ML, lazy_seq.ML, lazy_scan.ML;
src/HOL/Import/HOL4Setup.thy
--- 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 *}