[isabelle-dev] lex_prod changes

[Bertram Felgenhauer]

Hi,

I've gotten some emails from Jenkins lately and finally taken a moment
to investigate.

Apparently, R1 <*lex*> R2 was changed to artificially impose
irreflexivity on R1 (checking  a ~= a'  in addition to  a R1 a').

What are the benefits of doing this? There is a (heavy, to me)
downside: It destroys the property that the lexicographic product is
transitive if both input relations are. More fundamentally, while in
the previous formulation, the lexicographic product was a meaningful
and useful operation for quasi-orders, now that use case is closed
off.

Was this change discussed in advance? I may have missed it... in any
case I strongly dislike it.

Cheers,

Bertram