[isabelle-dev] Order Relations

[Lawrence Paulson]

It depends upon whether you regard having a carrier set as the norm or an exception. I think there are many natural constructions on relations that can only be done in the presence of a carrier set.
Larry

On 19 Feb 2013, at 02:50, Christian Sternagel <c.sternagel at gmail.com> wrote:

> My main problem with the current definition is that it is not (just) reflexivity, but rather reflexivity plus an additional property (that ensures that a relation is only defined on a domain). Why not split these in two separate predicates and use the second one only where really necessary?
> 
> I'm not sure how much work it would be to use this new definition of reflexivity. But if people think that what I say makes sense (or is more natural as reflexivity), I would give it a try and report afterwards.