src/HOL/Fun_Def.thy
changeset 55466 786edc984c98
parent 55085 0e8e4dc55866
child 55968 94242fa87638
     1.1 --- a/src/HOL/Fun_Def.thy	Fri Feb 14 07:53:45 2014 +0100
     1.2 +++ b/src/HOL/Fun_Def.thy	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -146,7 +146,7 @@
     1.4  
     1.5  lemmas [fundef_cong] =
     1.6    if_cong image_cong INT_cong UN_cong
     1.7 -  bex_cong ball_cong imp_cong Option.map_cong Option.bind_cong
     1.8 +  bex_cong ball_cong imp_cong map_option_cong Option.bind_cong
     1.9  
    1.10  lemma split_cong [fundef_cong]:
    1.11    "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q