On 02/19/2013 03:49 PM, Tobias Nipkow wrote:
Am 19/02/2013 03:50, schrieb Christian Sternagel:
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.
It sounds plausible to me, and I would be in favour of such a change assuming
that your application profits from it and the distribution does not suffer.
Well, currently my applications are all just based on different
definitions than those of Main, so there would be no direct gain.
Moreover, relations are represented by "('a * 'a) set" in some places,
whereas "'a => 'a => bool" (which I prefer, for some reason I'm not
quite able to put my finger on) is used in others.
In an ideal Isabelle/world I would expect a single definition of
reflexivity that is applicable everywhere and a clear convention for the
type of relations (including orderings) that is used uniformly (or at
least primarily). See. e.g., Ordering.thy vs. Relation.thy for the
current status.
I know that this might not be feasible right now, but who knows, with a
lot of small changes in the long run, it might be doable eventually?
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
