# HG changeset patch
# User bauerg
# Date 976107582 -3600
# Node ID 5cbb6e62c5020a09ee119bca7abe29eb379d2bfe
# Parent  620647438780e2ca3cd256f1c47192057158a12a
HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;

diff -r 620647438780 -r 5cbb6e62c502 NEWS
--- 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;