src/HOL/Recdef.thy
changeset 22622 25693088396b
parent 22399 80395c2c40cc
child 23150 073a65f0bc40
     1.1 --- a/src/HOL/Recdef.thy	Tue Apr 10 11:55:23 2007 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Tue Apr 10 14:11:01 2007 +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
     1.8 +imports Wellfounded_Relations FunDef
     1.9  uses
    1.10    ("../TFL/casesplit.ML")
    1.11    ("../TFL/utils.ML")
    1.12 @@ -64,11 +64,7 @@
    1.13    less_Suc_eq [THEN iffD2]
    1.14  
    1.15  lemmas [recdef_cong] = 
    1.16 -  if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
    1.17 -
    1.18 -lemma let_cong [recdef_cong]:
    1.19 -    "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"
    1.20 -  by (unfold Let_def) blast
    1.21 +  if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
    1.22  
    1.23  lemmas [recdef_wf] =
    1.24    wf_trancl