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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
