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
http://isabelle.in.tum.de/repos/isabelle/file/744934b818c7/src/HOL/Library/Cardinality.thy
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.

Andreas





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