Email Gateway (Oct 12 2020 at 17:46): Email Gateway (Oct 12 2020 at 17:46):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Email Gateway (Oct 19 2020 at 15:36):From: Makarius <makarius@sketis.net>
OK, it looks fine to me.
(I've got somehow used to a slightly complex/confusing situation, and have
lost the connection to people out there people out there who were trying to
use these interfaces.)
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Dec 21 2024 at 16:20 UTC