It’s obvious that this proposal should have been discussed more widely. And I shouldn’t have volunteered to implement it before securing firm offers of help, because it was obvious from the outset that it would be seriously laborious. With this change, a repair is never as simple as inserting some tactic or rewrite but requires at least a lemma or two. In some cases it’s a problem-solving task taking hours. So I’m sorry it’s taken me so long to reduce 60 failing entries to 20 (and I have fixes to five more in the pipeline). But I’d be happy to wash my hands of the whole thing.
Larry > On 21 Aug 2020, at 07:51, Jasmin Blanchette <[email protected]> wrote: > > 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. _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
