src/HOL/Library/Old_Recdef.thy
changeset 56248 67dc9549fa15
parent 55017 2df6ad1dbd66
child 58184 db1381d811ab
--- a/src/HOL/Library/Old_Recdef.thy	Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/Library/Old_Recdef.thy	Sat Mar 22 08:37:43 2014 +0100
@@ -77,7 +77,7 @@
   less_Suc_eq [THEN iffD2]
 
 lemmas [recdef_cong] =
-  if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
+  if_cong let_cong image_cong INF_cong SUP_cong bex_cong ball_cong imp_cong
   map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong 
 
 lemmas [recdef_wf] =