[isabelle-dev] Order of sublocale declarations
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.
More information about the isabelle-dev