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