[isabelle-dev] Order Relations
lp15 at cam.ac.uk
Tue Feb 19 12:43:51 CET 2013
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.
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.
More information about the isabelle-dev