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

[Andreas Schropp]

On 08/26/2011 06:50 PM, Tobias Nipkow wrote:
> I agree. Since predicates are primitive, starting from them is appropriate.
>
> Tobias

Did I get this right:
   the idea is to implement our advanced typedef via a HOL4-style 
predicate typedef?
That doesn't work because HOL4-style typedefs don't feature our extensions
to typedef and they are only conservative via a global theory 
transformation.

Or do you rather suggest having a predicate-based typedef with all our 
extensions?

Cheers,
   Andy