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

[Jasmin Christian Blanchette]

Am 25.08.2011 um 22:45 schrieb Florian Haftmann:

> HOL-Metis_Examples FAILED
> HOL-Nitpick_Examples FAILED

Adapting the Metis and Nitpick examples for a set constructor wouldn't be very difficult -- for Metis, it's mostly a matter of rerunning Sledgehammer to discover slightly different proofs if needed (or, worst case, comment out the offending examples), and for Nitpick it is just a technicality.

I can look into those things if and when it is decided to move to sets.

Jasmin