[isabelle-dev] Interpretation in arbitrary targets.

[Florian Haftmann]

Hi Clemens,

> I hope,
> though, it has become clear that I'm not opposed to having
> interpretation in locale contexts by principle, I'm merely opposed to
> explaining them in the way you propose.

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.

  context B
  begin

  sublocale EXPR

  end

  is equivalent

  to

  sublocale B < EXPR

Rationale: We have 30 occurences of sublocale in HOL/*.thy and 80%   and
more occur with the pattern

  context B
  begin
  …
  end

  sublocale B < EXPR

  context B
  begin
  …
  end

* 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.

Would this make sense?  I still think that the frontiers can be pushed
further, but this can still be a separate step, on which discussion can
be resumed after.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130414/c61a3456/attachment.sig>