author | bulwahn |
Sat, 09 Jul 2011 21:18:20 +0200 | |
changeset 43736 | d2f7af6e993c |
parent 43735 | 9b88fd07b912 |
child 43737 | 592b32eb18a6 |
child 43739 | 4529a3c56609 |
--- a/NEWS Sat Jul 09 21:09:09 2011 +0200 +++ b/NEWS Sat Jul 09 21:18:20 2011 +0200 @@ -60,6 +60,9 @@ *** HOL *** +* Archimedian_Field.thy: + constant field now is defined as parameter of a separate type class floor_ceiling. + * Finite_Set.thy: more coherent development of fold_set locales: locale fun_left_comm ~> locale comp_fun_commute