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.