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,