# [isabelle] Can't access to a sublocale theorem

Hi all,
I have two locales A and B. I set B as a sublocale of A. The problem I have is when trying to access to the "part" of B that comes from A. Here is an example:
locale A =
fixes A n
assumes as: g A n
locale B =
fixes A n
assumes bs: "g A n"
sublocale B < A
sorry
If I print the B locale I get:
locale elements:
fixes A :: "'a"
and n :: "'b"
assumes "PROP B A n"
notes A_axioms
=
(`PROP A A n`) [attribute <attribute>]
notes as
=
`?f A n`
notes B_axioms
=
(`PROP B A n`) [attribute <attribute>]
notes bs
=
`?g A n`
but I can't access to B.as
One way I found to solve this was:
context B begin
lemmas as = as
end
This solves the problem but produce a new one: when I set an interpretation of B, I get a "duplicate fact declaration" error. An obvious way to solve this is:
context B begin
lemmas as' = as
end
Is there any way to access to B.as with a renaming?
Thank you very much.
Hernan

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