changeset 59588 | c6f3dbe466b6 |
parent 59582 | 0fbed69ff081 |
parent 59587 | 8ea7b22525cb |
child 59621 | 291934bac95e |
--- a/NEWS Wed Mar 04 22:05:01 2015 +0100 +++ b/NEWS Wed Mar 04 23:31:13 2015 +0100 @@ -68,6 +68,11 @@ *** HOL *** +* removed functions "natfloor" and "natceiling", + use "nat o floor" and "nat o ceiling" instead. + A few of the lemmas have been retained and adapted: in their names + "natfloor"/"natceiling" has been replaced by "nat_floor"/"nat_ceiling". + * Qualified some duplicated fact names required for boostrapping the type class hierarchy: ab_add_uminus_conv_diff ~> diff_conv_add_uminus