On 08/26/2011 10:38 PM, Makarius wrote:
What is gained from that apart from having two versions of typedef?
I am with you here.
We don't need two primitive versions of typedefs.
The only thing that might be sensible from my POV is using predicates
instead of
sets in the primitive version (feat all your extensions) und simulating
the one using
axiomatized sets via composing Abs,Rep with the set-predicate-bijection.
But as I said: I can deal with axiomatized set with only minor
complications, so no
indication here.
Cheers,
Andy
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
