NEWS
changeset 30298 abefe1dfadbb
parent 30273 ecd6f0ca62ea
child 30300 aa44d67eea16
--- a/NEWS	Fri Mar 06 09:35:43 2009 +0100
+++ b/NEWS	Fri Mar 06 14:33:19 2009 +0100
@@ -220,6 +220,10 @@
 
 *** HOL ***
 
+* 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".
+
 * Auxiliary class "itself" has disappeared -- classes without any parameter
 are treated as expected by the 'class' command.