src/HOL/Recdef.thy
changeset 11533 0c0d2332e8f0
parent 11454 7514e5e21cb8
child 12023 d982f98e0f0d
     1.1 --- a/src/HOL/Recdef.thy	Fri Aug 31 16:27:43 2001 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Fri Aug 31 16:28:26 2001 +0200
     1.3 @@ -15,7 +15,9 @@
     1.4    ("../TFL/thry.ML")
     1.5    ("../TFL/tfl.ML")
     1.6    ("../TFL/post.ML")
     1.7 -  ("Tools/recdef_package.ML"):
     1.8 +  ("Tools/recdef_package.ML")
     1.9 +  ("Tools/basic_codegen.ML")
    1.10 +  ("Tools/inductive_codegen.ML"):
    1.11  
    1.12  lemma tfl_eq_True: "(x = True) --> x"
    1.13    by blast
    1.14 @@ -50,7 +52,11 @@
    1.15  use "../TFL/tfl.ML"
    1.16  use "../TFL/post.ML"
    1.17  use "Tools/recdef_package.ML"
    1.18 +use "Tools/basic_codegen.ML"
    1.19 +use "Tools/inductive_codegen.ML"
    1.20  setup RecdefPackage.setup
    1.21 +setup BasicCodegen.setup
    1.22 +setup InductiveCodegen.setup
    1.23  
    1.24  lemmas [recdef_simp] =
    1.25    inv_image_def