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) -----------------------------------