[isabelle-dev] Regression in the sublocale command
ballarin at in.tum.de
Thu Feb 19 20:17:43 CET 2015
Thanks for the clarification. So this is not a regression.
I had in fact overlooked that the rewrite rule had turned into reflexivity. Apologies for the confusion.
On 17 February, 2015 13:03 CET, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> > My conclusion of this discussion is that with 8fab871a2a6f the sublocale command immediately visits its target after the qed, which it didn't before. This now causes the command to loop. Is this correct?
> Yes, definitely.
> PGP available:
More information about the isabelle-dev