Re: [isabelle] Evaluation of List.coset



On Wed, 30 Jan 2013, 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?

Looking forward for Isabelle 2013 ;-),

You can start using Isabelle2013-RC2 right now, see again https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-January/msg00157.html

It also points to https://bitbucket.org/isabelle_project/isabelle-release which collects relevant information about this final stage before
lift-off of the final Isabelle2013 release.

Anything you see on the main Isabelle repository happening now is for the release after it (but 744934b818c7 mentioned above is from long ago).


	Makarius





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