On Thu, Aug 18, 2011 at 3:49 AM, Florian Haftmann < florian.haftm...@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.
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
