*** empty log message ***

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