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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
