HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;
authorbauerg
Wed Dec 06 13:59:42 2000 +0100 (2000-12-06)
changeset 106095cbb6e62c502
parent 10608 620647438780
child 10610 1dc640d06d19
HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;
NEWS
     1.1 --- a/NEWS	Wed Dec 06 13:22:58 2000 +0100
     1.2 +++ b/NEWS	Wed Dec 06 13:59:42 2000 +0100
     1.3 @@ -4,6 +4,8 @@
     1.4  
     1.5  *** Overview of INCOMPATIBILITIES ***
     1.6  
     1.7 +* HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;
     1.8 +
     1.9  * HOL: induct renamed to lfp_induct;
    1.10  
    1.11  * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;