Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Consolidated terminology and functio...

view this post on Zulip Email Gateway (Oct 12 2020 at 17:46):

From: 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

This hopefully eliminates some sources of confusion:

This refers to

view this post on Zulip Email Gateway (Oct 19 2020 at 15:36):

From: Makarius <>
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.)


isabelle-dev mailing list

Last updated: Apr 21 2024 at 01:10 UTC