| changeset 10609 | 5cbb6e62c502 |
| parent 10557 | dc615fccc1e6 |
| child 10634 | b4c3af8ebada |
--- a/NEWS Wed Dec 06 13:22:58 2000 +0100 +++ b/NEWS Wed Dec 06 13:59:42 2000 +0100 @@ -4,6 +4,8 @@ *** Overview of INCOMPATIBILITIES *** +* HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function; + * HOL: induct renamed to lfp_induct; * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;