--- a/NEWS Fri Mar 06 14:33:42 2009 +0100
+++ b/NEWS Fri Mar 06 14:51:18 2009 +0100
@@ -222,7 +222,7 @@
* New predicate "strict_mono" classifies strict functions on partial orders.
With strict functions on linear orders, reasoning about (in)equalities is
-facilitated by theorems "strict_mono_eq", "strict_mono_eq" and "strict_mono_eq".
+facilitated by theorems "strict_mono_eq", "strict_mono_less_eq" and "strict_mono_less".
* Auxiliary class "itself" has disappeared -- classes without any parameter
are treated as expected by the 'class' command.