NEWS
changeset 69708 1c201e4792cb
parent 69707 920fe0a2fd22
child 69709 7263b59219c1
     1.1 --- a/NEWS	Mon Jan 21 22:46:25 2019 +0100
     1.2 +++ b/NEWS	Mon Jan 21 07:08:27 2019 +0000
     1.3 @@ -134,6 +134,11 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Local_Theory.reset is no longer available in user space. Regular
     1.8 +definitional packages should use balanced blocks of
     1.9 +Local_Theory.open_target versus Local_Theory.close_target instead,
    1.10 +or the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY.
    1.11 +
    1.12  * Original PolyML.pointerEq is retained as a convenience for tools that
    1.13  don't use Isabelle/ML (where this is called "pointer_eq").
    1.14