Name bindings in locales should be treated uniformly regardless of the
background theory the locale happens to be in, so this can be
considered a defect in the implementation. My guess is that this is
caused by the full internal name containing theory information.
Otherwise I would expect the local theory active at the point of
declaration of the second theorem to reject binding the duplicate name.
On the other hand, if theory information is not stored in the internal
name, theory merges can result in invalid locales (that is, locales
that cannot even be activated, leaving alone interpreted).
Clemens
Quoting Florian Haftmann <[email protected]>:
Hi all,
currently, theorem names in locales can be shadowed (given that
declarations are in different theories, otherwise the foundation level
would reject the declaration since the two foundation theorems would
have the same name).
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.
Any comments?
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
