[isabelle-dev] Regression in the sublocale command

Clemens Ballarin ballarin at in.tum.de
Sat Feb 14 16:16:29 CET 2015


On 14 February, 2015 10:11 CET, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote: 
 
> I guess you found out using bisection.  But I read some incertainty in
> your words Ā»appears to have been introducedĀ«.  Is the changeset
> 8fab871a2a6f a reliable entrance point or a first approximation?

That particular problem is present in 8fab871a2a6f but not its parent (but who knows how often that behaviour changed in the history?)  It looks like there are more of these kinds of problems lurking, but unfortunately, I no longer fully understand the code, so I will have to rely on your help.  In particular, I would like to know what went wrong here.

Clemens
 




More information about the isabelle-dev mailing list