src/HOL/Typedef.thy
changeset 20426 9ffea7a8b31c
parent 19459 2041d472fc17
child 22846 fb79144af9a3
     1.1 --- a/src/HOL/Typedef.thy	Tue Aug 29 14:31:12 2006 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Tue Aug 29 14:31:13 2006 +0200
     1.3 @@ -7,7 +7,10 @@
     1.4  
     1.5  theory Typedef
     1.6  imports Set
     1.7 -uses ("Tools/typedef_package.ML") ("Tools/typedef_codegen.ML")
     1.8 +uses
     1.9 +  ("Tools/typedef_package.ML")
    1.10 +  ("Tools/typecopy_package.ML")
    1.11 +  ("Tools/typedef_codegen.ML")
    1.12  begin
    1.13  
    1.14  locale type_definition =
    1.15 @@ -83,8 +86,13 @@
    1.16  qed
    1.17  
    1.18  use "Tools/typedef_package.ML"
    1.19 +use "Tools/typecopy_package.ML"
    1.20  use "Tools/typedef_codegen.ML"
    1.21  
    1.22 -setup {* TypedefPackage.setup #> TypedefCodegen.setup *}
    1.23 +setup {*
    1.24 +  TypedefPackage.setup
    1.25 +  #> TypecopyPackage.setup
    1.26 +  #> TypedefCodegen.setup
    1.27 +*}
    1.28  
    1.29  end