[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Thu Aug 25 22:55:12 CEST 2011
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.
More information about the isabelle-dev