src/HOL/Datatype.thy
changeset 19564 d3e2f532459a
parent 19347 e2e709f3f955
child 19770 be5c23ebe1eb
     1.1 --- a/src/HOL/Datatype.thy	Fri May 05 16:50:58 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Fri May 05 17:17:21 2006 +0200
     1.3 @@ -6,7 +6,8 @@
     1.4  header {* Datatypes *}
     1.5  
     1.6  theory Datatype
     1.7 -imports Datatype_Universe
     1.8 +imports Datatype_Universe FunDef
     1.9 +uses ("Tools/function_package/fundef_datatype.ML")
    1.10  begin
    1.11  
    1.12  subsection {* Representing primitive types *}
    1.13 @@ -314,4 +315,9 @@
    1.14      ml (target_atom "SOME")
    1.15      haskell (target_atom "Just")
    1.16  
    1.17 +
    1.18 +use "Tools/function_package/fundef_datatype.ML"
    1.19 +setup FundefDatatype.setup
    1.20 +
    1.21 +
    1.22  end