| changeset 24422 | c0b5ff9e9e4d |
| parent 24342 | a1d489e254ec |
| child 24492 | de3fd08bb41c |
--- a/NEWS Fri Aug 24 14:14:17 2007 +0200 +++ b/NEWS Fri Aug 24 14:14:18 2007 +0200 @@ -635,6 +635,9 @@ *** HOL *** +* Formulation of theorem "dense" changed slightly due to integration with new +class dense_linear_order. + * theory Finite_Set: "name-space" locales Lattice, Distrib_lattice, Linorder etc. have disappeared; operations defined in terms of fold_set now are named Inf_fin, Sup_fin. INCOMPATIBILITY.