src/HOL/Recdef.thy
changeset 19770 be5c23ebe1eb
parent 19564 d3e2f532459a
child 22264 6a65e9b2ae05
     1.1 --- a/src/HOL/Recdef.thy	Mon Jun 05 14:22:58 2006 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Mon Jun 05 14:26:07 2006 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* TFL: recursive function definitions *}
     1.5  
     1.6  theory Recdef
     1.7 -imports Wellfounded_Relations Datatype
     1.8 +imports Wellfounded_Relations
     1.9  uses
    1.10    ("../TFL/casesplit.ML")
    1.11    ("../TFL/utils.ML")
    1.12 @@ -18,7 +18,6 @@
    1.13    ("../TFL/tfl.ML")
    1.14    ("../TFL/post.ML")
    1.15    ("Tools/recdef_package.ML")
    1.16 -  ("Tools/function_package/auto_term.ML")
    1.17  begin
    1.18  
    1.19  lemma tfl_eq_True: "(x = True) --> x"
    1.20 @@ -97,7 +96,4 @@
    1.21  qed
    1.22  
    1.23  
    1.24 -use "Tools/function_package/auto_term.ML"
    1.25 -setup FundefAutoTerm.setup
    1.26 -
    1.27  end