NEWS
changeset 43967 610efb6bda1f
parent 43940 26ca0bad226a
child 43970 3d204d261903
     1.1 --- a/NEWS	Sat Jul 23 23:33:59 2011 +0200
     1.2 +++ b/NEWS	Sun Jul 24 21:27:25 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