[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
schropp at in.tum.de
Fri Aug 26 22:23:36 CEST 2011
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
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
More information about the isabelle-dev