[isabelle-dev] Shadowing of theorem names in locales
ballarin at in.tum.de
Fri Mar 21 21:10:35 CET 2014
On 21 March, 2014 17:26 CET, Makarius <makarius at sketis.net> wrote:
> On Tue, 11 Feb 2014, Clemens Ballarin wrote:
> > For the processing of locale expression, facts are not really required.
> > Having all information related to syntax should be sufficient. I cannot
> > tell, though, whether facts may contain syntax in disguise of certain
> > attributes.
> In principle there could be arbitrary declarations disguised as
> declaration attributes of facts, but the general sanity assumption is that
> this is not done. The separate concept of syntax_declaration was
> introduced for that, when we sorted this out several years ago.
To be more precise about what I had said above: I actually believe that syntax is only required when parsing a locale (i.e. reading it for the first time). When activating it later, everything should be set, and the syntax should no longer matter.
More information about the isabelle-dev