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

[Andreas Schropp]

On 08/26/2011 07:08 PM, Brian Huffman wrote:
> As far as I understand, the typedef package merely issues global
> axioms of the form "type_definition Rep Abs S", as long as it is
> provided with a proof of "EX x. x : S".
>    

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 not really a problem, but complicates my conservativity
argument. Before local typedefs the proof of (EX x. x : A) was
global. Actually Makarius' attitude on this was that those non-emptiness
proofs "should be global most of the time", but he didn't want to
introduce a check.

Cheers,
   Andy