[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
schropp at in.tum.de
Thu Aug 25 22:49:54 CEST 2011
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!
More information about the isabelle-dev