1.1 --- a/NEWS	Sun Jun 30 11:37:34 2013 +0200
     1.2 +++ b/NEWS	Sun Jun 30 12:30:02 2013 +0200
     1.3 @@ -50,6 +50,11 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* System option "proofs" has been discontinued.  Instead the global
     1.8 +state of Proofterm.proofs is persistently compiled into logic images
     1.9 +as required, notably HOL-Proofs.  Users no longer need to change
    1.10 +Proofterm.proofs dynamically.  Minor INCOMPATIBILITY.
    1.11 +
    1.12  * Syntax translation functions (print_translation etc.) always depend
    1.13  on Proof.context.  Discontinued former "(advanced)" option -- this is
    1.14  now the default.  Minor INCOMPATIBILITY.