NEWS
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