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

[Andreas Schropp]

On 08/25/2011 10:45 PM, Florian Haftmann wrote:
> Hi all,
>
> thanks to many efforts (thanks particularly to Alex, Brian, Cezary,
> Larry) we already have gained some insights whether and how it would be
> technically possible to introduce a set type constructor.
>    

Let me ask something stupid:
   why exactly do you guys axiomatize 'a set?
Sure it's admissable and all, but why not do this definitionally
via the obvious typedef?

BTW: I am pretty ambivalent about this endeavour,
but  'a set  might be beneficial when postprocessing
results of the HOL->ZF translation. So good luck!

Cheers,
   Andy