haftmann [Wed, 22 May 2013 22:56:17 +0200] rev 52119
interpretation must always operate on the last element in a local theory stack, not on all elements: interpretated facts must disappear after pop from local theory stack, and transfer from last target is not enough
haftmann [Wed, 22 May 2013 22:56:17 +0200] rev 52118
mark local theory as brittle also after interpretation inside locales;
more correct bookkeeping on brittleness: must store directly beside lthy data, with implicit default true for levels > 1;
check brittleness only during context switch using (in ...) syntax, not for arbitrary exit of local theory