[isabelle-dev] lex_prod changes

[Jasmin Blanchette]

> On 20 Aug 2020, at 22:42, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
> As somebody who’s wasted a week trying to do this, I can’t say that I like it myself.

Well I hope you will revert it soon, because it breaks I don't know how many AFP entries, including two of mine.

I wish I would have answered to Stepan's original email to explain why his proposal wasn't a good one. Although I didn't design <*lex*>, having worked with orders and quasi-orders a bit, I can see why it's defined the way it is. When I saw "a ≠ a' " in the proposed revision, red flags went up, but I somehow forgot to follow up on that. Making such a change without checking how the definition is used in the AFP first, if that's what happened, strikes me as surprisingly native.

Jasmin