NEWS
changeset 22218 30a8890d2967
parent 22152 df787d582323
child 22316 f662831459de
     1.1 --- a/NEWS	Wed Jan 31 14:03:31 2007 +0100
     1.2 +++ b/NEWS	Wed Jan 31 16:05:10 2007 +0100
     1.3 @@ -507,11 +507,17 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Dropped lemma duplicate def_imp_eq in favor of meta_eq_to_obj_eq.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10 +* Dropped lemma duplicate if_def2 in favor of if_bool_eq_conj.
    1.11 +INCOMPATIBILITY.
    1.12 +
    1.13  * Added syntactic class "size"; overloaded constant "size" now has
    1.14  type "'a::size ==> bool"
    1.15  
    1.16  * Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op
    1.17 -dvd" to "Divides.div", "Divides.mod" and
    1.18 +dvd" to "Divides.div", "Divides.mod" and "Divides.dvd"
    1.19  "Divides.dvd". INCOMPATIBILITY.
    1.20  
    1.21  * Added method "lexicographic_order" automatically synthesizes