# HG changeset patch
# User haftmann
# Date 1283945122 -7200
# Node ID 7b2631c91a95cb5dd8eac540dc053b5719557e3b
# Parent  49fc6c842d6cdbec4cb489f7a25add57661f2faf
NEWS

diff -r 49fc6c842d6c -r 7b2631c91a95 NEWS
--- a/NEWS	Wed Sep 08 13:22:24 2010 +0200
+++ b/NEWS	Wed Sep 08 13:25:22 2010 +0200
@@ -65,6 +65,9 @@
 Sign.root_path and Sign.local_path may be applied directly where this
 feature is still required for historical reasons.
 
+* Discontinued ancient 'constdefs' command.  INCOMPATIBILITY, use
+'definition' instead.
+
 
 *** HOL ***