[isabelle-dev] Order of sublocale declarations

[Amine Chaieb]

Thanks Andreas. Does this mean that this sublocale scenario is 
prohibited? And if so, is it due to technical reasons or is there a 
fundamental problem here?

Amine.

On 01/31/2013 02:04 PM, Andreas Lochbihler wrote:
> Hi Amine,
>
> the error message in the second case is only delayed: You get it, once 
> you open the AB context again (context AB begin). In the first case, 
> it shows up immediately, because the sublocale command already 
> constructs the context AB enriched with B.
>
> Best,
> Andreas