| changeset 30198 | 922f944f03b2 |
| parent 30181 | 05629f28f0f7 |
| child 30200 | 0db3a35eab01 |
--- a/NEWS Mon Mar 02 08:26:03 2009 +0100 +++ b/NEWS Mon Mar 02 16:53:55 2009 +0100 @@ -348,6 +348,9 @@ etc. slightly changed. Some theorems named order_class.* now named preorder_class.*. +* HOL/Relation: +Renamed "refl" to "refl_on", "reflexive" to "refl, "diag" to "Id_on". + * HOL/Finite_Set: added a new fold combinator of type ('a => 'b => 'b) => 'b => 'a set => 'b Occasionally this is more convenient than the old fold combinator which is