# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1453198765 -3600
# Node ID eca7b38c8ee5cd5e6dccb1486835be2444fb20f7
# Parent  67792e4a548663b483cd684c1f4a19714798e62f
Added approximation of powr to NEWS/CONTRIBUTORS

diff -r 67792e4a5486 -r eca7b38c8ee5 CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Jan 19 07:59:29 2016 +0100
+++ b/CONTRIBUTORS	Tue Jan 19 11:19:25 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.
diff -r 67792e4a5486 -r eca7b38c8ee5 NEWS
--- a/NEWS	Tue Jan 19 07:59:29 2016 +0100
+++ b/NEWS	Tue Jan 19 11:19:25 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)