[isabelle-dev] Regression in the sublocale command

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Tue Feb 17 13:03:34 CET 2015


> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150217/24172e26/attachment.sig>


More information about the isabelle-dev mailing list