[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 

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 

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 

Is there any way to access to B.as with a renaming? 

Thank you very much. 


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