NEWS
authorhaftmann
Wed, 08 Sep 2010 13:25:22 +0200
changeset 39215 7b2631c91a95
parent 39214 49fc6c842d6c
child 39217 1d5e81f5f083
child 39246 9e58f0499f57
NEWS
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 ***