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

Cezary Kaliszyk cezarykaliszyk at gmail.com
Sat Aug 27 00:18:41 CEST 2011

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:
to Isabelle-set. With it, Quotient_Examples succeeds.


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

More information about the isabelle-dev mailing list