Hi Florian,
I'm investigating a regression which prevents identifying certain equivalent
locales through circular sublocale declarations:
sublocale loc1 < x: loc2 A c (* sigma_1 *)
where "x.b == B" and "x.d == e" (* tau_1 *)
sorry
sublocale loc2 < x: loc1 A b (* sigma_2 *)
where "x.c == C" and "x.e == d" (* tau_2 *)
sorry (* loops from changeset 8fab871a2a6f *)
The last "sorry" loops, which is unfortunate, because it forces certain
workarounds on my current project. In a fairly lengthy debug session I figured
out that it is the simplifier that loops. This is an indication that the
morphisms tau_1 and tau_2 are applied simultaneously, which they should not.
In any case, the behaviour appears to have been introduced quite a while ago in
8fab871a2a6f, which is in the first batch of your changes to the locale
interpretation commands.
Clemens
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
