On 21 March, 2014 17:26 CET, Makarius <makar...@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. Clemens _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
