src/HOL/Import/HOL4Setup.thy
changeset 17801 30cbd2685e73
parent 17322 781abf7011e6
child 19064 bf19cc5a7899
     1.1 --- a/src/HOL/Import/HOL4Setup.thy	Sat Oct 08 22:39:38 2005 +0200
     1.2 +++ b/src/HOL/Import/HOL4Setup.thy	Sat Oct 08 22:39:39 2005 +0200
     1.3 @@ -4,7 +4,8 @@
     1.4  *)
     1.5  
     1.6  theory HOL4Setup imports MakeEqual
     1.7 -  uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
     1.8 +  uses "susp.ML" "lazy_seq.ML" "lazy_scan.ML"
     1.9 +    ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
    1.10  
    1.11  section {* General Setup *}
    1.12