[isabelle] Two orders / class instantiations



Hello,
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.