changeset 70957 | aa41be39aa99 |
parent 70950 | 7378fa1d0892 |
child 71134 | 81536e5d8ea7 |
--- a/NEWS Sun Oct 27 20:07:59 2019 -0400 +++ b/NEWS Sun Oct 27 20:11:30 2019 -0400 @@ -83,6 +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. + *** ML *** * Theory construction may be forked internally, the operation