Re: [isabelle] [isabelle-dev] Relations vs. Predicates

Hi Christian,

> actually I was talking about the development version (hence the dev
> list) but the situation is essentially the same in Isabelle2011-1 I
> guess. By "adhoc overloading" I was referring to the theory
> Adhoc_Overloading (e.g., used for do-notation) which could (I think) be
> used to unify the syntax (independently from what you said about generic
> lemmas) of funpow, relpow, compow, and what is more.

this won't work: Adhoc_Overloading can only disambiguate disjoint type
signatures (neglecting sort constraints).  But the generic power operation

	nat => 'a => 'a

and the set-relational one

	nat => 'a set => 'a set

do overlap (subst 'a := 'a set).



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.