NEWS
changeset 39215 7b2631c91a95
parent 39199 720112792ba0
child 39239 47273e5b1441
child 39250 548a3e5521ab
     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