[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sat Sep 3 11:19:39 CEST 2011

Hi again,

thanks Alex for the summary.

> So, it seems that we can conclude that instead of the nice unified
> development that we hoped for in 2008, we got quite a bit of confusion
> (points 1.1 and 1.2), in addition to the drawbacks that were already
> known (1.3, 1.5-1.6). If we had to choose between the two versions now
> (with no status quo to consider), the case would be pretty clear. So
> the question is whether our users out there will tolerate that they
> have to fix quite a number of theories.

following the discussions it appears that we have settled to reintroduce
'a set – after the next release.

I will now examine HOL-Nominal more closer, and after that come up with
a next report about the distribution.  The intermediate state can always
be inspected at


Concerning AFP, the discussion with Viorel (partially of-list) has
reminded me that we should trust our users more and not try to convert
AFP entries silently without contacting them previously.  Already the
feedback has a value on its own:

Nevertheless, here a repository clone where single adaptions might go at
a later time, although I would be lucky not to need it:





PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110903/abbe75c8/attachment.asc>

More information about the isabelle-dev mailing list