Let me just make some remarks as a user. At ITP 2011 I published a paper http://www21.in.tum.de/~nipkow/pubs/itp11.html where I showed how to use locales to structure stepwise development of modules (see p11). In that context I intentionally used the notation
interpretation (in A) B-expr instead of sublocale in an implementation step. Of course I comment on the deviation in the notation saying that I have chosen this variation of interpretation because it is more intuitive (see p10). I do find it more intuitive because it tells me clearly what is going on: some locale expression is interpreted in some locale. And this is also how you explain sublocale in your locale tutorial. Hence Florian's suggestions made a lot of sense to me. Tobias Am 17/04/2013 22:28, schrieb Clemens Ballarin: > Quoting Makarius <makar...@sketis.net>: > >> On Fri, 12 Apr 2013, Clemens Ballarin wrote: >> >>> That sounds a bit dogmatic. If additional commands are made available for >>> targets, then the syntax should clearly be more flexible if better intuition >>> can be achieved. >> >> That is just a matter of modularity of concepts: the older "(in a)" notation >> was slightly generalized at some point to allow named contexts as sketched >> above, and the relation between the two is as pointed out by Florian. > > I am aware of the modularity aspect of this. My criticism is that deviations > from the current approach in favour of preferable notation are not even > considered. In any case, I'm not sure how useful the old notation still is. > Maybe it can be given up at some point. > > Clemens > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev