Re: [isabelle] Evaluation of List.coset

Hi Jesus,

On 01/30/2013 10:36 AM, Jesus Aransay wrote:
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?
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.
There's no enumeration involved.


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