changeset 44589 | d2f7af6e993c |
parent 44580 | 717e96cf9527 |
child 44590 | 592b32eb18a6 |
1.1 --- a/NEWS Sat Jul 09 21:09:09 2011 +0200 1.2 +++ b/NEWS Sat Jul 09 21:18:20 2011 +0200 1.3 @@ -60,6 +60,9 @@ 1.4 1.5 *** HOL *** 1.6 1.7 +* Archimedian_Field.thy: 1.8 + constant field now is defined as parameter of a separate type class floor_ceiling. 1.9 + 1.10 * Finite_Set.thy: more coherent development of fold_set locales: 1.11 1.12 locale fun_left_comm ~> locale comp_fun_commute