```Dear Hernan,

```
it seems to me that you are trying to use locales other than the "official" way. Noramlly, you should never need to access the theorems in a locale when the context does not contain the locale. (Although there are some special cases when this does not work, but then, you lose all support from the locale system.)
```Why do you have to access as outside the context of B and its interpretations?

```
Every local leaves a trace of its declarations in the global theory context, which is what you are trying to utilize: A.as is the trace declaring the assumption "g A n" in locale A. Thus, there is no B.as as B does not declare a theorem as by itself. If you declare theorems with the same name multiple times, you get into trouble, as you have experienced yourself.
```
Note that A.as refers to the theorem

A ?A.0 ?n ==> g ?A.0 n

i.e., there is an explicit premise that states the assumptions of locale A.

```
When working with locales, you usually never refer to the declarations in the global theory context - even if the global terms show up in output buffers. Instead, prove your lemmas in the context B or interpret B for specific parameters first (either globally with interpretation or locally in an Isar proof with interpret). Then, you can access as without prefixes.
```
Hope this helps,
Andreas

Hernan Ponce-De-Leon schrieb:
```
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`
```

```
```
```
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
```
```
```
```
Thank you very much.
```
```
Hernan
```
--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
```
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft
```

```

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