src/HOL/Recdef.thy

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