[isabelle-dev] Regression in the sublocale command

[Clemens Ballarin]

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.

Clemens

 
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.
> 
> 	Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>