1.1 --- a/NEWS	Wed Sep 08 13:22:24 2010 +0200
     1.2 +++ b/NEWS	Wed Sep 08 13:25:22 2010 +0200
     1.3 @@ -65,6 +65,9 @@
     1.4  Sign.root_path and Sign.local_path may be applied directly where this
     1.5  feature is still required for historical reasons.
     1.6  
     1.7 +* Discontinued ancient 'constdefs' command.  INCOMPATIBILITY, use
     1.8 +'definition' instead.
     1.9 +
    1.10  
    1.11  *** HOL ***
    1.12