[isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

This view is correct, but it is not the whole story.  Since the system  
maintains a graph of interpretations and follows them transitively,  
the effect achieved by

   sublocale locale < expression

is much like

   instance class < sort

of the old user interface to type classes.  This relationship is  
discussed in the new paper (Section 5.2).

Clemens


Quoting Tobias Nipkow <nipkow at in.tum.de>:

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