src/HOL/Typedef.thy
changeset 31723 f5cafe803b55
parent 29797 08ef36ed2f8a
child 37863 7f113caabcf4
     1.1 --- a/src/HOL/Typedef.thy	Thu Jun 18 18:31:14 2009 -0700
     1.2 +++ b/src/HOL/Typedef.thy	Fri Jun 19 17:23:21 2009 +0200
     1.3 @@ -7,8 +7,8 @@
     1.4  theory Typedef
     1.5  imports Set
     1.6  uses
     1.7 -  ("Tools/typedef_package.ML")
     1.8 -  ("Tools/typecopy_package.ML")
     1.9 +  ("Tools/typedef.ML")
    1.10 +  ("Tools/typecopy.ML")
    1.11    ("Tools/typedef_codegen.ML")
    1.12  begin
    1.13  
    1.14 @@ -115,8 +115,8 @@
    1.15  
    1.16  end
    1.17  
    1.18 -use "Tools/typedef_package.ML" setup TypedefPackage.setup
    1.19 -use "Tools/typecopy_package.ML" setup TypecopyPackage.setup
    1.20 +use "Tools/typedef.ML" setup Typedef.setup
    1.21 +use "Tools/typecopy.ML" setup Typecopy.setup
    1.22  use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
    1.23  
    1.24  end