[isabelle-dev] NEWS: Consolidated terminology and function signatures for nested targets

[Florian Haftmann]

Consolidated terminology and function signatures for nested targets:

  * Local_Theory.begin_nested replaces Local_Theory.open_target.

  * Local_Theory.end_nested replaces Local_Theory.close_target.

  * Combination of Local_Theory.begin_nested and
    Local_Theory.end_nested(_result) replaces
    Local_Theory.subtarget(_result).

This hopefully eliminates some sources of confusion:

* Clear distinction in terminology between the single main (bottom)
target and the arbitrary number of nested targets.

* Separation of the primitives for package development (in module
Local_Theory) and the traditional embedding into the Isar language using
context … begin … end blocks (in module Target_Context).

This refers to http://isabelle.in.tum.de/repos/isabelle/rev/e4dde7beab39


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