# HG changeset patch
# User nipkow
# Date 1453199769 -3600
# Node ID 6acae6430fccfdf092e6a4a3411a5941f085719b
# Parent  eca7b38c8ee5cd5e6dccb1486835be2444fb20f7# Parent  e5bc7cbb0bcca8fa49d35deb989e73035cd24fb4
merged

diff -r e5bc7cbb0bcc -r 6acae6430fcc CONTRIBUTORS
--- 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.
diff -r e5bc7cbb0bcc -r 6acae6430fcc NEWS
--- 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)