[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.