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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
