[isabelle-dev] Regression in the sublocale command
florian.haftmann at informatik.tu-muenchen.de
Sat Feb 14 21:43:09 CET 2015
> 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.
Can you point me to a source position where you get stuck? Doing a
short revisitation of the history, I found out that my only change to
the machinery itself has been 54795:e58623a33ba5. The refinement of the
commands and their integration with local theories happened smoothly on
the surface level, and it should not be that difficult to step through
it after some guidance through the typical indirections of the local
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev