| changeset 52148 | 893b15200ec1 |
| parent 52141 | eff000cab70f |
| parent 52143 | 36ffe23b25f8 |
| child 52266 | 86d6f57c2c1e |
--- a/NEWS Sat May 25 15:44:29 2013 +0200 +++ b/NEWS Sat May 25 18:30:38 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.