Re: [isabelle] Evaluation of List.coset
On 01/30/2013 10:36 AM, Jesus Aransay wrote:
No, I have adapted Cardinality such that equality and subset between
sets and complements can be evaluated (cf. changeset 9014e78ccde2),
provided that the element type instatiates the new type class card_UNIV.
In the Isabelle development version I observed that the file
"Cardinality.thy" has suffered some changes related to the behaviour
of "List.coset"; more concretely, the line 467 in
proves some results about "List.coset" of enumerated types "by eval";
does this means that in the incoming release of Isabelle 2013
"List.coset" will be really evaluated for "enum" types?
There's no enumeration involved.
This archive was generated by a fusion of
Pipermail (Mailman edition) and