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