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

Andreas Schropp 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 
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.


More information about the isabelle-dev mailing list