NEWS
changeset 51002 496013a6eb38
parent 50994 aafd4270b4d4
child 51088 0a55ac5bdd92
--- a/NEWS	Thu Jan 31 12:09:07 2013 +0100
+++ b/NEWS	Thu Jan 31 17:42:12 2013 +0100
@@ -4,6 +4,12 @@
 New in this Isabelle version
 ----------------------------
 
+*** HOL ***
+
+* Theory "RealVector" and "Limits": Introduce type class
+(lin)order_topology. Allows to generalize theorems about limits and
+order. Instances are reals and extended reals.
+
 
 New in Isabelle2013 (February 2013)
 -----------------------------------