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

[Alexander Krauss]

> The global axiom is
>
> EX x. x : A ==> type_definition Rep Abs A
>
> allowing local typedefs whenever non-emptiness of A is
> derivable, even using assumptions in the context.

This is an interesting discussion, but totally off-topic in this thread 
(whose main content is already growing very large.)

Please start a separate thread, if you want to continue...

Thanks,
Alex