*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] real_vector*From*: Steve W <s.wong.731 at gmail.com>*Date*: Tue, 22 Mar 2011 16:54:32 +0000

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

**Follow-Ups**:**Re: [isabelle] real_vector***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] Problems with linear orders and strings
- Next by Date: Re: [isabelle] real_vector
- Previous by Thread: [isabelle] Isabelle wants you for the Google Summer of Code 2011
- Next by Thread: Re: [isabelle] real_vector
- Cl-isabelle-users March 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list