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

Andreas Schropp 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 mailing list