changeset 58541 | 48e23e342415 |
parent 58540 | 872f330a0f8a |
parent 58512 | dc4d76dfa8f0 |
child 58551 | 9986fb541c87 |
--- a/NEWS Sat Oct 04 22:15:22 2014 +0200 +++ b/NEWS Sat Oct 04 22:15:31 2014 +0200 @@ -38,6 +38,9 @@ *** HOL *** +* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1 +Minor INCOMPATIBILITY. + * Bootstrap of listsum as special case of abstract product over lists. Fact rename: listsum_def ~> listsum.eq_foldr