On Sun, 7 Oct 2012, Florian Haftmann wrote:
After some pondering I would argue that this should be forbidden: * (Complete) shadowing is a constant source of confusion. * Global interpretations are impossible then, since they would result in two global theorems with the same name.
I've started some experiments with this idea and will report the empirical results soon ...
Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev