changeset 52143 | 36ffe23b25f8 |
parent 52116 | abf9fcfa65cf |
child 52148 | 893b15200ec1 |
--- a/NEWS Sat May 25 15:00:53 2013 +0200 +++ b/NEWS Sat May 25 15:37:53 2013 +0200 @@ -40,6 +40,10 @@ *** Pure *** +* Syntax translation functions (print_translation etc.) always depend +on Proof.context. Discontinued former "(advanced)" option -- this is +now the default. Minor INCOMPATIBILITY. + * Target-sensitive commands 'interpretation' and 'sublocale'. Particulary, 'interpretation' now allows for non-persistent interpretation within "context ... begin ... end" blocks.