NEWS
changeset 26315 cb3badaa192e
parent 26231 cd9d7f449369
child 26323 73efc70edeef
--- a/NEWS	Tue Mar 18 20:33:28 2008 +0100
+++ b/NEWS	Tue Mar 18 20:33:29 2008 +0100
@@ -40,6 +40,12 @@
 
 *** HOL ***
 
+* Theory Nat: renamed less_imp_le to less_imp_le_nat; removed
+redundant lemmas less_trans, less_linear, le_imp_less_or_eq,
+le_less_trans, less_le_trans, which merely duplicate lemmas of the
+same name in theory Orderings.  Potential INCOMPATIBILITY due to more
+general and different variable names.
+
 * Library/Option_ord.thy: Canonical order on option type.
 
 * Library/RBT.thy: New theory of red-black trees, an efficient