[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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