slightly clearer formulation

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

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