[isabelle-dev] lex_prod changes

[Klein, Gerwin (Data61, Kensington NSW)]

> On 21 Aug 2020, at 14:51, Jasmin Blanchette <j.c.blanchette at vu.nl> wrote:
> 
>> 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.

That, and if doing it despite errors, not fixing the AFP simultaneously. That is pretty bad form. 

If we wait with reverting, authors might already start fixing their entries to the new definition. So the earlier the better.

Cheers,
Gerwin