--- a/CONTRIBUTORS Tue Jan 19 11:36:02 2016 +0100
+++ b/CONTRIBUTORS Tue Jan 19 11:36:09 2016 +0100
@@ -6,6 +6,10 @@
Contributions to Isabelle2016
-----------------------------
+* Winter 2016: Manuel Eberl, TUM
+ Support for real exponentiation ("powr") in the "approximation" method.
+ (This was removed in Isabelle 2015 due to a changed definition of "powr")
+
* Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
Proof of the central limit theorem: includes weak convergence,
characteristic functions, and Levy's uniqueness and continuity theorem.
--- a/NEWS Tue Jan 19 11:36:02 2016 +0100
+++ b/NEWS Tue Jan 19 11:36:09 2016 +0100
@@ -1236,6 +1236,9 @@
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)