--- a/CONTRIBUTORS Tue Jul 01 16:26:14 2014 +0200
+++ b/CONTRIBUTORS Tue Jul 01 16:08:31 2014 +0100
@@ -32,6 +32,9 @@
Permanent interpretation inside theory, locale and class targets
with mixin definitions.
+* Spring 2014: Lawrence C Paulson, Cambridge
+ Theory Complex_Basic_Analysis. Tidying up Number_Theory vs Old_Number_Theory
+
* Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI
Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
--- a/NEWS Tue Jul 01 16:26:14 2014 +0200
+++ b/NEWS Tue Jul 01 16:08:31 2014 +0100
@@ -205,6 +205,13 @@
INCOMPATIBILITY.
+* Revisions to HOL/Number_Theory
+ - consolidated the proofs of the binomial theorem
+ - the function fib is again of type nat=>nat and not overloaded
+ - no more references to Old_Number_Theory in the HOL libraries (except the AFP)
+
+INCOMPATIBILITY.
+
* Swapped orientation of facts image_comp and vimage_comp:
image_compose ~> image_comp [symmetric]