[isabelle] Two orders / class instantiations

is it possible to have two class instantiations with two different relations for the same type?ÂFor example having (set, \subset) p.o. and also having (set, \supset) p.o. ?ÂFor the moment it seems not, but how do I proceed if I need both orders in a theorem?ÂThank you!

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