[isabelle-dev] Order of sublocale declarations

Amine Chaieb amine at chaieb.org
Thu Jan 31 14:56:46 CET 2013

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?


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

More information about the isabelle-dev mailing list