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