--- a/NEWS Thu Dec 13 16:48:07 2001 +0100
+++ b/NEWS Thu Dec 13 16:48:34 2001 +0100
@@ -1,4 +1,3 @@
-
Isabelle NEWS -- history user-relevant changes
==============================================
@@ -224,6 +223,10 @@
a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be
necessary to attach explicit type constraints;
+* HOL/Relation: the prefix name of the infix "O" has been changed from "comp"
+to "rel_comp"; INCOMPATIBILITY: a few theorems have been renamed accordingly
+(eg "compI" -> "rel_compI").
+
* HOL: syntax translations now work properly with numerals and records
expressions;