# HG changeset patch
# User nipkow
# Date 968222371 -7200
# Node ID 53e2a8bce258e927152159cfe8a9299fff7ceda0
# Parent  2374ba026fc6ab2a0b86206503dee878e875affc
*** empty log message ***

diff -r 2374ba026fc6 -r 53e2a8bce258 NEWS
--- 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,