# HG changeset patch
# User wenzelm
# Date 973880417 -3600
# Node ID abeefb0a79aefea06efda63397da0798e4b7207a
# Parent  226d474e644df8dbf66543bcae56281e908a4cf2
* added overloaded operations "inverse" and "divide" (infix "/");

diff -r 226d474e644d -r abeefb0a79ae NEWS
--- a/NEWS	Fri Nov 10 19:18:37 2000 +0100
+++ b/NEWS	Fri Nov 10 19:20:17 2000 +0100
@@ -1,3 +1,4 @@
+
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
@@ -57,6 +58,8 @@
 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
 
+* added overloaded operations "inverse" and "divide" (infix "/");
+
 * >, >= and \<ge> can now be used for input; they are immediately replaced
   by the converse symbol, eg "x > y" by "y < x".