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