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

Reply via email to