[isabelle-dev] lex_prod changes

Klein, Gerwin (Data61, Kensington NSW) Gerwin.Klein at data61.csiro.au
Fri Aug 21 11:59:07 CEST 2020

I’m happy with either direction as long as we get into a consistent state. If we revert the definition, we’ll also have to revert the AFP fixes, but I’m assuming that this is going to be easier than the other direction.


> On 21 Aug 2020, at 17:55, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 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 <lp15 at cam.ac.uk> 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
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list