[isabelle-dev] Regression in the sublocale command

Clemens Ballarin ballarin at in.tum.de
Sun Feb 15 11:59:56 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?

Clemens





More information about the isabelle-dev mailing list