Before wasting another week, which incidentally I really can’t spare, it would be nice to know whether there are any objections to going back to the original definition?
Larry > On 21 Aug 2020, at 09:34, Lawrence Paulson <[email protected]> wrote: > > 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. _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
