--- 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)