NEWS
changeset 59587 8ea7b22525cb
parent 59570 7ee382059c94
child 59588 c6f3dbe466b6
--- a/NEWS	Tue Mar 03 19:08:04 2015 +0100
+++ b/NEWS	Wed Mar 04 23:31:04 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