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

Alexander Krauss krauss at in.tum.de
Fri Aug 26 22:53:04 CEST 2011

> 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...


More information about the isabelle-dev mailing list