# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1404227311 -3600
# Node ID 250decee4ac51e1172f7eed5a0a3dd94a7afa2c9
# Parent  d3eac6fd0bd61a8e72ca52979ee8776d1375cbd4
for new release

diff -r d3eac6fd0bd6 -r 250decee4ac5 CONTRIBUTORS
--- 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.
 
diff -r d3eac6fd0bd6 -r 250decee4ac5 NEWS
--- 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]