# [isabelle] type unification failed using an old lemma?

Hi,
Sorry in advance if this is some trivial error on my part.

`I'd like to use the lemma has_vector_derivative_mult in the HOL library
``which reads:
`
"lemma has_vector_derivative_mult[derivative_intros]:

` "(f has_vector_derivative f') (at x within s) â (g
``has_vector_derivative g') (at x within s) â
`` ((Îx. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a ::
``real_normed_algebra)) (at x within s)"
`` by (rule bounded_bilinear.has_vector_derivative[OF
``bounded_bilinear_mult])"
`
However it seems that using a statement such as

`have "((Îx. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a
``:: real_normed_algebra)) (at x within {a .. b})"
`
leads to a standard type unification error:
Type unification failed: Clash of types "_ â _" and "real"
Type error in application: incompatible operand type
Operator: op * (f x) :: real â real
Operand: g' :: real â real
Coercion Inference:
Local coercion insertion on the operand failed:
No coercion known for type constructors: "fun" and "real"
Am I missing something or is the lemma itself flawed?

`As an aside, there is a similar lemma for the has_derivative operator:
``has_derivative_mult
`which works for statements like

`have "((%x. f x * g x) has_derivative (%y. f x * g' y + f' y * g x))
``(at x within {a .. b})"
``Say I have h=(%x. f x * g x), I can obtain h' such that h has_derivative
``h but can't seem to define h' explicitly.
`
Thanks,
Alex Hicks

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*