NEWS
changeset 12489 c92e38c3cbaa
parent 12472 3307149f1ec2
child 12538 150af0a4bb11
     1.1 --- a/NEWS	Thu Dec 13 16:48:07 2001 +0100
     1.2 +++ b/NEWS	Thu Dec 13 16:48:34 2001 +0100
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -224,6 +223,10 @@
     1.9  a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be
    1.10  necessary to attach explicit type constraints;
    1.11  
    1.12 +* HOL/Relation: the prefix name of the infix "O" has been changed from "comp"
    1.13 +to "rel_comp"; INCOMPATIBILITY: a few theorems have been renamed accordingly
    1.14 +(eg "compI" -> "rel_compI").
    1.15 +
    1.16  * HOL: syntax translations now work properly with numerals and records
    1.17  expressions;
    1.18