[isabelle] real_vector



Hi,

I'm looking at how "real_vector" is used as a type and am somewhat confused
by examples like:

definition
  convex :: "'a::real_vector set \<Rightarrow> bool" ...

in HOL/Library/Convex.thy. How come "convex" is declared wrt the type
variable "'a" rather than "real_vector" directly, i.e.

convex :: "real_vector set..."

Thank you for any help.

Steve




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