[isabelle] reasoning about classes of many-sorted structures



Hello, 

As far as I see, type classes do not allow multiple type
variables.  Concretely, say I
want to reason about vector spaces (K,V,+,*,...)  without having either of K and V fixed.  Is there any elegant way around this?    

Thank you in advance for any hint, 
   Andrei Popescu







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