1.1 --- a/src/HOL/Recdef.thy	Fri Dec 02 16:05:31 2005 +0100
     1.2 +++ b/src/HOL/Recdef.thy	Fri Dec 02 16:43:42 2005 +0100
     1.3 @@ -63,7 +63,8 @@
     1.4    same_fst_def
     1.5    less_Suc_eq [THEN iffD2]
     1.6  
     1.7 -lemmas [recdef_cong] = if_cong image_cong
     1.8 +lemmas [recdef_cong] = 
     1.9 +  if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
    1.10  
    1.11  lemma let_cong [recdef_cong]:
    1.12      "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"