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

Andreas Schropp schropp at in.tum.de
Fri Aug 26 18:36:50 CEST 2011

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 

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


More information about the isabelle-dev mailing list