src/HOL/Recdef.thy
changeset 31723 f5cafe803b55
parent 29654 24e73987bfe2
child 32244 a99723d77ae0
     1.1 --- a/src/HOL/Recdef.thy	Thu Jun 18 18:31:14 2009 -0700
     1.2 +++ b/src/HOL/Recdef.thy	Fri Jun 19 17:23:21 2009 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    ("Tools/TFL/thry.ML")
     1.5    ("Tools/TFL/tfl.ML")
     1.6    ("Tools/TFL/post.ML")
     1.7 -  ("Tools/recdef_package.ML")
     1.8 +  ("Tools/recdef.ML")
     1.9  begin
    1.10  
    1.11  text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
    1.12 @@ -76,8 +76,8 @@
    1.13  use "Tools/TFL/thry.ML"
    1.14  use "Tools/TFL/tfl.ML"
    1.15  use "Tools/TFL/post.ML"
    1.16 -use "Tools/recdef_package.ML"
    1.17 -setup RecdefPackage.setup
    1.18 +use "Tools/recdef.ML"
    1.19 +setup Recdef.setup
    1.20  
    1.21  lemmas [recdef_simp] =
    1.22    inv_image_def