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

Makarius makarius at sketis.net
Mon Oct 19 17:36:27 CEST 2020


On 12/10/2020 19:46, Florian Haftmann wrote:
> 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 refers to http://isabelle.in.tum.de/repos/isabelle/rev/e4dde7beab39

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


More information about the isabelle-dev mailing list