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