changeset 56248 | 67dc9549fa15 |
parent 55968 | 94242fa87638 |
child 56643 | 41d3596d8a64 |
--- a/src/HOL/Fun_Def.thy Fri Mar 21 22:54:16 2014 +0100 +++ b/src/HOL/Fun_Def.thy Sat Mar 22 08:37:43 2014 +0100 @@ -144,7 +144,7 @@ unfolding Let_def by blast lemmas [fundef_cong] = - if_cong image_cong INT_cong UN_cong + if_cong image_cong INF_cong SUP_cong bex_cong ball_cong imp_cong map_option_cong Option.bind_cong lemma split_cong [fundef_cong]: