for new release
authorpaulson <lp15@cam.ac.uk>
Tue Jul 01 16:08:31 2014 +0100 (2014-07-01)
changeset 57474250decee4ac5
parent 57455 d3eac6fd0bd6
child 57475 d328664394ab
for new release
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Jul 01 16:26:14 2014 +0200
     1.2 +++ b/CONTRIBUTORS	Tue Jul 01 16:08:31 2014 +0100
     1.3 @@ -32,6 +32,9 @@
     1.4    Permanent interpretation inside theory, locale and class targets
     1.5    with mixin definitions.
     1.6  
     1.7 +* Spring 2014: Lawrence C Paulson, Cambridge
     1.8 +  Theory Complex_Basic_Analysis. Tidying up Number_Theory vs Old_Number_Theory
     1.9 +
    1.10  * Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI
    1.11    Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
    1.12  
     2.1 --- a/NEWS	Tue Jul 01 16:26:14 2014 +0200
     2.2 +++ b/NEWS	Tue Jul 01 16:08:31 2014 +0100
     2.3 @@ -205,6 +205,13 @@
     2.4  
     2.5  INCOMPATIBILITY.
     2.6  
     2.7 +* Revisions to HOL/Number_Theory
     2.8 +  - consolidated the proofs of the binomial theorem
     2.9 +  - the function fib is again of type nat=>nat and not overloaded
    2.10 +  - no more references to Old_Number_Theory in the HOL libraries (except the AFP)
    2.11 +
    2.12 +INCOMPATIBILITY.
    2.13 +
    2.14  * Swapped orientation of facts image_comp and vimage_comp:
    2.15  
    2.16    image_compose ~> image_comp [symmetric]