Email Gateway (Feb 17 2026 at 11:31): Email Gateway (Feb 17 2026 at 11:31):From: Daniel Kirchner <cl-isabelle-users@lists.cam.ac.uk>
Hi all,
I'm a bit confused about the recursive behaviour of the polarity of
unbundle in nested bundles. Consider the following snippet:
bundle A
begin
notation implies (infix "->" 25)
end
bundle B
begin
unbundle A
end
term "a -> b" (* expected: doesn't parse *)
unbundle B
term "a -> b" (* expected: parses *)
unbundle no B
term "a -> b" (* unexpected: still parses! *)
unbundle no A
term "a -> b" (* only now fails to parse again *)
isar-ref.pdf states for the no-prefix of bundles that "This also works
recusively for the unbundle command as declaration inside a bundle
definition: no means that both the order and polarity of declarations
is reversed"
So shouldn't "unbundle no B" entail "unbundle no A" resulting in the
notation to already vanish in the third "term" above? It actually
appears to be the case that "unbundle no B" even causes "unbundle A"
instead of "unbundle no A" (replace "unbundle B" with "unbundle no B"
in the snippet above and the behaviour remains exactly the same).
It would be useful to be able to define several fine-grained bundles
and then combine them into a compound bundle, but due to this
behaviour, that doesn't seem to work as expected.
Interestingly, for "unbundle no" within bundles, reversing the polarity
does seem to work, so this works as expected:
bundle A
begin
notation implies (infix "->" 25)
end
bundle B
begin
unbundle no A
end
term "a -> b" (* as expected: doesn't parse *)
unbundle no B
term "a -> b" (* as expected: parses *)
unbundle B
term "a -> b" (* as expected: doesn't parse *)
Is this a bug or am I misunderstanding something here? If the latter,
is there another way to define a bundle C consisting of several other
bundles, s.t. "unbundle C" unbundles all of them, while "unbundle no C"
causes "unbundle no" for all of them?
Best wishes,
Daniel
Last updated: Feb 22 2026 at 05:16 UTC