src/HOL/Basic_BNFs.thy
changeset 56077 d397030fb27e
parent 55945 e96383acecf9
child 58446 e89f57d1e46c
     1.1 --- a/src/HOL/Basic_BNFs.thy	Thu Mar 13 08:56:08 2014 +0100
     1.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Mar 13 08:56:08 2014 +0100
     1.3 @@ -175,7 +175,7 @@
     1.4    thus "f \<circ> x = g \<circ> x" by auto
     1.5  next
     1.6    fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
     1.7 -  unfolding image_def comp_def[abs_def] by auto
     1.8 +    by (auto simp add: fun_eq_iff)
     1.9  next
    1.10    show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
    1.11    apply (rule card_order_csum)