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 relationsh
* 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 Pro
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 :
Hi Clemens,
I still see us disagree on how far the loca
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 dis
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 thi
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
