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.sterna...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
