NEWS
changeset 9871 53e2a8bce258
parent 9835 543d23cd1259
child 9908 7c7ff65b6846
--- 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,