# [isabelle] bundle commands inside a locale

Hi,
I am trying to find a way to encapsulate all the notations that are defined inside a locale into a separate bundle. For a locale called "Foo", this would allow me to toggle the notation whenever I unfold "Foo" using the "interpretaion" or "sublocale" command inside another locale called "Bar".
## locale Foo =
## fixes A :: "'a => bool"
## assumes "P A"
## begin
##
## (*let's say I define some notation here*)
## definition
## t :: "'a => bool" ("TTT _" [50])
## where
## "t == A"
##
## lemma "TTT x ⟹ A x" unfolding t_def .
##
## end
##
## locale Bar =
## fixes B :: "'a => bool"
## assumes a1:"P B" and "Q B"
## begin
##
## interpretation Foo B using a1 .
##
## (*the syntax is lost here. TTT not recognized anymore...
## lemma "TTT x ⟹ B x"*)
##
## (* assuming that I could create a bundle inside Foo locale,
## how can I include the Foo_syntax bundle here? ...*)
##
## end
Note that I am aware of the possibility to define bundle blocks that include some notation commands like bellow. However, this is only applicable for those terms which are not defined inside a locale.
## definition "t == True"
##
## bundle Foo_syntax
## begin
## notation t ("TTT" [50])
## end
What I am looking for is a way to wrap "notation" command inside an inline "bundle" inside a locale as follows:
## context Foo
## begin
##
## bundle Foo_syntax = {
## notation t ("TTT" [50]),
## (*or any other command here...*)
## }
##
## end
Thanks in advance for your help. :)
-- an Isabelle user

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*