Added approximation of powr to NEWS/CONTRIBUTORS
authorManuel Eberl <eberlm@in.tum.de>
Tue Jan 19 11:19:25 2016 +0100 (2016-01-19)
changeset 62201eca7b38c8ee5
parent 62200 67792e4a5486
child 62203 6acae6430fcc
Added approximation of powr to NEWS/CONTRIBUTORS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Jan 19 07:59:29 2016 +0100
     1.2 +++ b/CONTRIBUTORS	Tue Jan 19 11:19:25 2016 +0100
     1.3 @@ -6,6 +6,10 @@
     1.4  Contributions to Isabelle2016
     1.5  -----------------------------
     1.6  
     1.7 +* Winter 2016: Manuel Eberl, TUM
     1.8 +  Support for real exponentiation ("powr") in the "approximation" method.
     1.9 +  (This was removed in Isabelle 2015 due to a changed definition of "powr")
    1.10 +
    1.11  * Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
    1.12    Proof of the central limit theorem: includes weak convergence,
    1.13    characteristic functions, and Levy's uniqueness and continuity theorem.
     2.1 --- a/NEWS	Tue Jan 19 07:59:29 2016 +0100
     2.2 +++ b/NEWS	Tue Jan 19 11:19:25 2016 +0100
     2.3 @@ -1236,6 +1236,9 @@
     2.4  method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
     2.5  examples.
     2.6  
     2.7 +* HOL-Decision_Procs: The "approximation" method works with "powr" 
     2.8 +  (exponentiation on real numbers) again.
     2.9 +
    2.10  * HOL-Probability: Reworked measurability prover
    2.11    - applies destructor rules repeatedly
    2.12    - removed application splitting (replaced by destructor rule)