[isabelle] Cset Supremum in Isabelle2011



Hello,

I have been successfully been using FSet theory included in development
releases for executable finite sets. In Isabelle2011 it has been renamed
to Cset.

Collecting all elements of a set of sets was possible in development
releases and the command
value "Supremum (Fset.Set [Fset.Set[1::nat, 2], Fset.Set[2, 3]])"
returned "Fset.Set [1, 2, 3]".

However, in Isabelle2011 the command
value "Supremum (Cset.set [Cset.set[1::nat, 2], Cset.set[2, 3]])"
fails with the message:
*** Wellsortedness error:
*** Type nat Cset.set not of sort complete_lattice
*** No type arity nat :: enum
although, there is
instantiation Cset.set :: (type) complete_lattice
which does not mention the class enum.

Any suggestions?

Best regards,
Filip






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