summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 62237 | 167641f8b83a |

parent 62235 | 3687c199e22b |

child 62253 | 91363e4c196d |

1.1 --- a/NEWS Sun Jan 24 12:33:40 2016 +0100 1.2 +++ b/NEWS Sun Jan 24 13:07:50 2016 +0100 1.3 @@ -708,6 +708,9 @@ 1.4 import of parent, as for general 'locale' expressions. INCOMPATIBILITY, 1.5 remove '!' and add '?' as required. 1.6 1.7 +* HOL-Decision_Procs: The "approximation" method works with "powr" 1.8 +(exponentiation on real numbers) again. 1.9 + 1.10 * HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm with Contour 1.11 integrals (= complex path integrals), Cauchy's integral theorem, winding 1.12 numbers and Cauchy's integral formula, Liouville theorem, Fundamental 1.13 @@ -1249,9 +1252,6 @@ 1.14 method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for 1.15 examples. 1.16 1.17 -* HOL-Decision_Procs: The "approximation" method works with "powr" 1.18 - (exponentiation on real numbers) again. 1.19 - 1.20 * HOL-Probability: Reworked measurability prover 1.21 - applies destructor rules repeatedly 1.22 - removed application splitting (replaced by destructor rule)