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

[Andreas Schropp]

On 08/26/2011 10:38 PM, Makarius wrote:
> What is gained from that apart from having two versions of typedef?

I am with you here.
We don't need two primitive versions of typedefs.

The only thing that might be sensible from my POV is using predicates 
instead of
sets in the primitive version (feat all your extensions) und simulating 
the one using
axiomatized sets via composing Abs,Rep with the set-predicate-bijection.
But as I said: I can deal with axiomatized set with only minor 
complications, so no
indication here.

Cheers,
   Andy