src/HOL/BNF_FP_Base.thy
changeset 56684 d8f32f55e463
parent 56651 fc105315822a
child 56846 9df717fef2bb
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Fri Apr 25 11:58:10 2014 +0200
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Fri Apr 25 12:09:15 2014 +0200
     1.3 @@ -166,10 +166,7 @@
     1.4  lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
     1.5    by (erule arg_cong)
     1.6  
     1.7 -lemma snd_o_convol: "(snd \<circ> (\<lambda>x. (f x, g x))) = g"
     1.8 -  by (rule ext) simp
     1.9 -
    1.10 -lemma inj_on_convol_id: "inj_on (\<lambda>x. (x, f x)) X"
    1.11 +lemma inj_on_convol_ident: "inj_on (\<lambda>x. (x, f x)) X"
    1.12    unfolding inj_on_def by simp
    1.13  
    1.14  lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"