8 
8 
9 * Winter 2016: Manuel Eberl, TUM 
9 * Winter 2016: Manuel Eberl, TUM 
10 Support for real exponentiation ("powr") in the "approximation" method. 
10 Support for real exponentiation ("powr") in the "approximation" method. 
11 (This was removed in Isabelle 2015 due to a changed definition of "powr") 
11 (This was removed in Isabelle 2015 due to a changed definition of "powr") 
12 
12 
13 * Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM 

14 Proof of the central limit theorem: includes weak convergence, 

15 characteristic functions, and Levy's uniqueness and continuity theorem. 

16 

17 * Summer 2015  Winter 2016: Lawrence C Paulson, Cambridge 
13 * Summer 2015  Winter 2016: Lawrence C Paulson, Cambridge 
18 General, homology form of Cauchy's integral theorem and supporting material 
14 General, homology form of Cauchy's integral theorem and supporting material 
19 (ported from HOL Light). 
15 (ported from HOL Light). 
20 
16 
21 * Winter 2015/16: Gerwin Klein, NICTA 
17 * Winter 2015/16: Gerwin Klein, NICTA 
22 New print_record command. 
18 New print_record command. 

19 

20 * May  December 2015: Makarius Wenzel 

21 Prover IDE improvements. 

22 More Isar language elements. 

23 Document language refinements. 

24 Poly/ML debugger integration. 

25 Improved multiplatform and multiarchitecture support. 
23 
26 
24 * Winter 2015: Manuel Eberl, TUM 
27 * Winter 2015: Manuel Eberl, TUM 
25 The radius of convergence of power series and various summability tests. 
28 The radius of convergence of power series and various summability tests. 
26 Harmonic numbers and the EulerMascheroni constant. 
29 Harmonic numbers and the EulerMascheroni constant. 
27 The Generalised Binomial Theorem. 
30 The Generalised Binomial Theorem. 
57 
60 
58 * Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich 
61 * Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich 
59 Command to lift a BNF structure on the raw type to the abstract type for 
62 Command to lift a BNF structure on the raw type to the abstract type for 
60 typedefs. 
63 typedefs. 
61 
64 

65 * Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM 

66 Proof of the central limit theorem: includes weak convergence, 

67 characteristic functions, and Levy's uniqueness and continuity theorem. 

68 
62 
69 
63 Contributions to Isabelle2015 
70 Contributions to Isabelle2015 
64  
71  
65 
72 
66 * 2014/2015: Daniel Matichuk, Toby Murray, NICTA and Makarius Wenzel 
73 * 2014/2015: Daniel Matichuk, Toby Murray, NICTA and Makarius Wenzel 