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] =