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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
