[isabelle-dev] Regression in the sublocale command

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

More information about the isabelle-dev mailing list