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,
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 named targets including
classes or just locales?
it will work within locales, and thus within type classes.
* Equip interpretation in non-theory targets to allow confined,
non-persistent interpretations.
context B
begin
interpretation EXPR
end
would not add a dependency to B.
Here, it's not clear whether the interpretation just wouldn't add a
dependency, or wouldn't modify B at all.
It should not modify B at all -- with the restriction that ad-hoc
contexts currently may leak nontheless in certain situations (cf.
Makarius' statement).
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
