summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 24 Jan 2016 13:07:50 +0100 | |

changeset 62237 | 167641f8b83a |

parent 62236 | 3a326bc9d4d8 |

child 62238 | 3cde0ea64727 |

proper NEWS for this release;

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