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
Hi Clemens,
I still see us disagree on how far the local theory game can be driven
wrt. interpretation, nevertheless I can imagine that there is an
intermediate road map which we can agree on:
* Extend sublocale for use within locale targets s.t.
This is fine with me. Will this work for
I was under the impression that type synonyms are expanded in typ
antiquotations, but apparently not, at least not with 30624dab6054. If I write
@{typ vname} I get vname, even if vname is a type synonym for string. Maybe it
has always been like this, but it means that one cannot automatically
Hi Florian,
OK, then we agree on this.
Please let me know if you need to make changes to locales.ML. I want
to make sure that routes out of certain quirks there don't get blocked
accidentally.
Clemens
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:
Hi Clemens,
* Simplifier tactics and tools use proper Proof.context instead of
historic type simpset. Old-style declarations like addsimps,
addsimprocs etc. operate directly on Proof.context. Raw type simpset
retains its use as snapshot of the main Simplifier context, using
simpset_of and put_simpset on
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
