> I agree that a separate theory would be nice. But before doing so, we
> should also try to consolidate what's there already. The current state
> in List.thy is as follows (8c0a27b9c1bd):
>
> 1. lexord :: ('a * 'a) set => ('a list * 'a list) set
>a set version of the irreflexive lexicographic
Hi Florian,
> Just a remark on
> http://isabelle.in.tum.de/repos/isabelle/rev/8c0a27b9c1bd: the matter on
> lexicographic orderings in List.thy is now numerous enough but still
> self-contained to justify a separate theory Lexorder.thy.
I agree that a separate theory would be nice. But before do
Just a remark on
http://isabelle.in.tum.de/repos/isabelle/rev/8c0a27b9c1bd: the matter on
lexicographic orderings in List.thy is now numerous enough but still
self-contained to justify a separate theory Lexorder.thy. I would also
suggest that the predicate version should be done using locales rath
