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