> On 21 Aug 2020, at 14:51, Jasmin Blanchette <[email protected]> wrote: > >> On 20 Aug 2020, at 22:42, Lawrence Paulson <[email protected]> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
