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

[Cezary Kaliszyk]

On Thu, Aug 18, 2011 at 3:49 AM, Florian Haftmann <
florian.haftmann at informatik.tu-muenchen.de> wrote:

> [...] So, the best way now is
> to continue eliminating set-pred mixture (also in the AFP of course!)
> and discover problems in packages – I'm a little concerned about
> quotient since this has been introduced after 2008, but maybe Cezary can
> comment on this.


Hi Florian,

I already made the changes to the core of the quotient package as of:
http://isabelle.in.tum.de/repos/isabelle/rev/3cdc4176638c

With the above the quotient package works both as is and with the
explicit set type.

It seems you included only a part of the above changeset in the
isabelle_set repository, in particular the change in the
src/HOL/Equiv_Relations.thy is necessary but seems it did not go in.
With this change the quotient package works and only changes to the
particular examples may be needed, but many work without any changes:

New Nominal: Works.

Quotient_Message: Works.
Quotient_Int: Works.
FSet: Requires removing one 'simp add: mem_def', then works.
DList: I pushed a change 5 min ago; with it it works.

CSet and List_Cset depend on Library/More_Set which doesn't load, so
I can't say if there are any quotient issues...

AFP/Coinductive needs updating, long before quotients it does:
  enat_set :: "enat => bool" so I can't say without going further in the
  code.

Regards,

Cezary.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110818/8721e53f/attachment-0002.html>