src/HOL/Import/HOL4Setup.thy
changeset 16417 9bc16273c2d4
parent 14620 1be590fd2422
child 17322 781abf7011e6
     1.1 --- a/src/HOL/Import/HOL4Setup.thy	Fri Jun 17 11:35:35 2005 +0200
     1.2 +++ b/src/HOL/Import/HOL4Setup.thy	Fri Jun 17 16:12:49 2005 +0200
     1.3 @@ -3,8 +3,8 @@
     1.4      Author:     Sebastian Skalberg (TU Muenchen)
     1.5  *)
     1.6  
     1.7 -theory HOL4Setup = MakeEqual
     1.8 -  files ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML"):
     1.9 +theory HOL4Setup imports MakeEqual
    1.10 +  uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
    1.11  
    1.12  section {* General Setup *}
    1.13