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