src/HOL/Typedef.thy
changeset 38393 7c045c03598f
parent 37863 7f113caabcf4
child 38536 7e57a0dcbd4f
     1.1 --- a/src/HOL/Typedef.thy	Thu Aug 12 13:53:42 2010 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Thu Aug 12 17:56:41 2010 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  imports Set
     1.5  uses
     1.6    ("Tools/typedef.ML")
     1.7 -  ("Tools/typecopy.ML")
     1.8    ("Tools/typedef_codegen.ML")
     1.9  begin
    1.10  
    1.11 @@ -116,7 +115,6 @@
    1.12  end
    1.13  
    1.14  use "Tools/typedef.ML" setup Typedef.setup
    1.15 -use "Tools/typecopy.ML" setup Typecopy.setup
    1.16  use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
    1.17  
    1.18  end