| changeset 71147 | 2e46c0b4042d |
| parent 71134 | 81536e5d8ea7 |
| child 71149 | a7d1fb0c9e16 |
--- a/NEWS Thu Nov 21 13:25:27 2019 +0100 +++ b/NEWS Thu Nov 21 15:22:24 2019 +0100 @@ -83,8 +83,9 @@ * Theory Complete_Lattices: renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf -* Session HOL-Analysis: Method "metric" implements a decision procedure -for simple linear statements in metric spaces. +* Session HOL-Analysis: proof method "metric" implements a decision +procedure for simple linear statements in metric spaces. + *** ML ***