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

[Cezary Kaliszyk]

On Fri, Aug 26, 2011 at 5:45 AM, Florian Haftmann <
florian.haftmann at informatik.tu-muenchen.de> wrote:
>
> [...] According to my knowledge, the following session produce
> problems: [...]
> HOL-Quotient_Examples FAILED
>

Please propagare the isabelle changeset:
http://isabelle.in.tum.de/repos/isabelle/rev/5e0f9e0e32fb
to Isabelle-set. With it, Quotient_Examples succeeds.

Cheers,

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