src/HOL/Library/FinFun.thy
changeset 53374 a14d2a854c02
parent 52916 5f3faf72b62a
child 55565 f663fc1e653b
     1.1 --- a/src/HOL/Library/FinFun.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -960,7 +960,7 @@
     1.4      { fix g' a b show "Abs_finfun (g \<circ> op $ g'(a $:= b)) = (Abs_finfun (g \<circ> op $ g'))(a $:= g b)"
     1.5        proof -
     1.6          obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
     1.7 -        moreover hence "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
     1.8 +        moreover from g' have "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
     1.9          moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto)
    1.10          ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def)
    1.11        qed }