Moved code generator setup from Recdef to Inductive.
authorberghofe
Mon Dec 10 15:17:49 2001 +0100 (2001-12-10)
changeset 124376d4e02b6dd43
parent 12436 a2df07fefed7
child 12438 afd41635dcf9
Moved code generator setup from Recdef to Inductive.
src/HOL/Inductive.thy
src/HOL/Recdef.thy
     1.1 --- a/src/HOL/Inductive.thy	Mon Dec 10 15:16:49 2001 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Mon Dec 10 15:17:49 2001 +0100
     1.3 @@ -9,11 +9,14 @@
     1.4  theory Inductive = Gfp + Sum_Type + Relation
     1.5  files
     1.6    ("Tools/inductive_package.ML")
     1.7 +  ("Tools/inductive_codegen.ML")
     1.8    ("Tools/datatype_aux.ML")
     1.9    ("Tools/datatype_prop.ML")
    1.10    ("Tools/datatype_rep_proofs.ML")
    1.11    ("Tools/datatype_abs_proofs.ML")
    1.12    ("Tools/datatype_package.ML")
    1.13 +  ("Tools/datatype_codegen.ML")
    1.14 +  ("Tools/recfun_codegen.ML")
    1.15    ("Tools/primrec_package.ML"):
    1.16  
    1.17  
    1.18 @@ -69,6 +72,9 @@
    1.19  
    1.20  text {* Package setup. *}
    1.21  
    1.22 +use "Tools/recfun_codegen.ML"
    1.23 +setup RecfunCodegen.setup
    1.24 +
    1.25  use "Tools/datatype_aux.ML"
    1.26  use "Tools/datatype_prop.ML"
    1.27  use "Tools/datatype_rep_proofs.ML"
    1.28 @@ -76,7 +82,12 @@
    1.29  use "Tools/datatype_package.ML"
    1.30  setup DatatypePackage.setup
    1.31  
    1.32 +use "Tools/datatype_codegen.ML"
    1.33 +setup DatatypeCodegen.setup
    1.34 +
    1.35 +use "Tools/inductive_codegen.ML"
    1.36 +setup InductiveCodegen.setup
    1.37 +
    1.38  use "Tools/primrec_package.ML"
    1.39 -setup PrimrecPackage.setup
    1.40  
    1.41  end
     2.1 --- a/src/HOL/Recdef.thy	Mon Dec 10 15:16:49 2001 +0100
     2.2 +++ b/src/HOL/Recdef.thy	Mon Dec 10 15:17:49 2001 +0100
     2.3 @@ -15,9 +15,7 @@
     2.4    ("../TFL/thry.ML")
     2.5    ("../TFL/tfl.ML")
     2.6    ("../TFL/post.ML")
     2.7 -  ("Tools/recdef_package.ML")
     2.8 -  ("Tools/basic_codegen.ML")
     2.9 -  ("Tools/inductive_codegen.ML"):
    2.10 +  ("Tools/recdef_package.ML"):
    2.11  
    2.12  lemma tfl_eq_True: "(x = True) --> x"
    2.13    by blast
    2.14 @@ -52,11 +50,7 @@
    2.15  use "../TFL/tfl.ML"
    2.16  use "../TFL/post.ML"
    2.17  use "Tools/recdef_package.ML"
    2.18 -use "Tools/basic_codegen.ML"
    2.19 -use "Tools/inductive_codegen.ML"
    2.20  setup RecdefPackage.setup
    2.21 -setup BasicCodegen.setup
    2.22 -setup InductiveCodegen.setup
    2.23  
    2.24  lemmas [recdef_simp] =
    2.25    inv_image_def