| changeset 72450 | 24bd1316eaae |
| parent 72388 | 633d14bd1e59 |
| child 72451 | e51f1733618d |
--- a/NEWS Mon Oct 12 07:25:38 2020 +0000 +++ b/NEWS Mon Oct 12 07:25:38 2020 +0000 @@ -55,6 +55,14 @@ * Definitions in locales produce rule which can be added as congruence rule to protect foundational terms during simplification. +* 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. + +INCOMPATIBILITY. + *** HOL ***