src/HOL/Recdef.thy
changeset 12437 6d4e02b6dd43
parent 12023 d982f98e0f0d
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Recdef.thy	Mon Dec 10 15:16:49 2001 +0100
     1.2 +++ b/src/HOL/Recdef.thy	Mon Dec 10 15:17:49 2001 +0100
     1.3 @@ -15,9 +15,7 @@
     1.4    ("../TFL/thry.ML")
     1.5    ("../TFL/tfl.ML")
     1.6    ("../TFL/post.ML")
     1.7 -  ("Tools/recdef_package.ML")
     1.8 -  ("Tools/basic_codegen.ML")
     1.9 -  ("Tools/inductive_codegen.ML"):
    1.10 +  ("Tools/recdef_package.ML"):
    1.11  
    1.12  lemma tfl_eq_True: "(x = True) --> x"
    1.13    by blast
    1.14 @@ -52,11 +50,7 @@
    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