Re: [isabelle] real_vector

On Wed, 23 Mar 2011 07:19:54 Johannes Hölzl wrote:
> 1) The types in the type class real_vector only contain vectors
> of reals. So it is not necessary to specify this explicitly.
>    it is enough to say:
>    consts v :: "'a real_vector"

Do you mean this?

consts v :: "'a::real_vector"


Attachment: signature.asc
Description: This is a digitally signed message part.

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