[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
florian.haftmann at informatik.tu-muenchen.de
Sat Sep 3 11:19:39 CEST 2011
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:
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev