| changeset 69709 | 7263b59219c1 |
| parent 69708 | 1c201e4792cb |
| child 69733 | 6d158fd15b85 |
--- a/NEWS Mon Jan 21 07:08:27 2019 +0000 +++ b/NEWS Mon Jan 21 07:08:55 2019 +0000 @@ -139,6 +139,9 @@ Local_Theory.open_target versus Local_Theory.close_target instead, or the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY. +* Slightly more conventional naming schema in structure Inductive. +Minor INCOMPATIBILITY. + * Original PolyML.pointerEq is retained as a convenience for tools that don't use Isabelle/ML (where this is called "pointer_eq").