1.1 --- a/NEWS	Wed Sep 06 08:04:41 2000 +0200
     1.2 +++ b/NEWS	Wed Sep 06 08:39:31 2000 +0200
     1.3 @@ -37,6 +37,8 @@
     1.4  * HOL: removed obsolete theorem binding expand_if (refer to split_if
     1.5  instead);
     1.6  
     1.7 +* HOL: less_induct is renamed nat_less_induct
     1.8 +
     1.9  * HOL/Real: "rabs" replaced by overloaded "abs" function;
    1.10  
    1.11  * HOL/ML: even fewer consts are declared as global (see theories Ord,