--- a/CONTRIBUTORS Sun Jan 24 12:33:09 2016 +0100
+++ b/CONTRIBUTORS Sun Jan 24 12:33:40 2016 +0100
@@ -10,10 +10,6 @@
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.
-
* Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge
General, homology form of Cauchy's integral theorem and supporting material
(ported from HOL Light).
@@ -21,6 +17,13 @@
* Winter 2015/16: Gerwin Klein, NICTA
New print_record command.
+* May - December 2015: Makarius Wenzel
+ Prover IDE improvements.
+ More Isar language elements.
+ Document language refinements.
+ Poly/ML debugger integration.
+ Improved multi-platform and multi-architecture support.
+
* Winter 2015: Manuel Eberl, TUM
The radius of convergence of power series and various summability tests.
Harmonic numbers and the Euler-Mascheroni constant.
@@ -59,6 +62,10 @@
Command to lift a BNF structure on the raw type to the abstract type for
typedefs.
+* 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.
+
Contributions to Isabelle2015
-----------------------------