NEWS
changeset 43970 3d204d261903
parent 43957 64f88ef1835e
parent 43967 610efb6bda1f
child 44015 a1507f567de6
     1.1 --- a/NEWS	Mon Jul 25 14:10:12 2011 +0200
     1.2 +++ b/NEWS	Mon Jul 25 23:27:20 2011 +0200
     1.3 @@ -79,6 +79,10 @@
     1.4    SUPR_apply ~> SUP_apply
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Theorem collections ball_simps and bex_simps do not contain theorems referring
     1.8 +to UNION any longer;  these have been moved to collection UN_ball_bex_simps.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * Archimedian_Field.thy:
    1.12      floor now is defined as parameter of a separate type class floor_ceiling.
    1.13