OK. So, just to make sure that I get this right: for locales A and B
where A contains the theorem a
context B begin
context begin
interpretation x: A
end
theorems b = x.a
end
would enrich B by b but not x.a, right?
Clemens
Quoting Florian Haftmann <[email protected]>:
context B begin
context
begin
interpretation A
end
end
This looks attractive, but could you please elaborate the semantics:
- What would be the effect of the interpretation from the inner block on
the outer block?
The interpretation would only affect the inner block.
- What would be the effect of the entire sequence on B?
None.
In other words, you can think of
context B
begin
...
interpretation A
...
end
being equivalent to
context B
begin
...
context
begin
interpretation A
...
end
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
