NEWS
changeset 57474 250decee4ac5
parent 57452 ecad2a53755a
child 57476 dc542b78ef0f
     1.1 --- a/NEWS	Tue Jul 01 16:26:14 2014 +0200
     1.2 +++ b/NEWS	Tue Jul 01 16:08:31 2014 +0100
     1.3 @@ -205,6 +205,13 @@
     1.4  
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Revisions to HOL/Number_Theory
     1.8 +  - consolidated the proofs of the binomial theorem
     1.9 +  - the function fib is again of type nat=>nat and not overloaded
    1.10 +  - no more references to Old_Number_Theory in the HOL libraries (except the AFP)
    1.11 +
    1.12 +INCOMPATIBILITY.
    1.13 +
    1.14  * Swapped orientation of facts image_comp and vimage_comp:
    1.15  
    1.16    image_compose ~> image_comp [symmetric]