NEWS
changeset 12489 c92e38c3cbaa
parent 12472 3307149f1ec2
child 12538 150af0a4bb11
--- 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;