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).

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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