src/HOL/FunDef.thy
changeset 40108 dbab949c2717
parent 37767 a2b7a20d6ea3
child 46526 c4cf9d03c352
     1.1 --- a/src/HOL/FunDef.thy	Sat Oct 23 23:41:19 2010 +0200
     1.2 +++ b/src/HOL/FunDef.thy	Sat Oct 23 23:42:04 2010 +0200
     1.3 @@ -5,11 +5,10 @@
     1.4  header {* Function Definitions and Termination Proofs *}
     1.5  
     1.6  theory FunDef
     1.7 -imports Wellfounded
     1.8 +imports Partial_Function Wellfounded
     1.9  uses
    1.10    "Tools/prop_logic.ML"
    1.11    "Tools/sat_solver.ML"
    1.12 -  ("Tools/Function/function_lib.ML")
    1.13    ("Tools/Function/function_common.ML")
    1.14    ("Tools/Function/context_tree.ML")
    1.15    ("Tools/Function/function_core.ML")
    1.16 @@ -101,7 +100,6 @@
    1.17    "wf R \<Longrightarrow> wfP (in_rel R)"
    1.18    by (simp add: wfP_def)
    1.19  
    1.20 -use "Tools/Function/function_lib.ML"
    1.21  use "Tools/Function/function_common.ML"
    1.22  use "Tools/Function/context_tree.ML"
    1.23  use "Tools/Function/function_core.ML"