[isabelle-dev] Interpretation in arbitrary targets.

[Tobias Nipkow]

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 <makarius at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev