| changeset 59536 | 03bde055a1a0 |
| parent 59511 | ef65605a7d9c |
| child 59555 | 05573e5504a9 |
--- a/NEWS Sat Feb 14 10:24:15 2015 +0100 +++ b/NEWS Sat Feb 14 10:24:15 2015 +0100 @@ -68,6 +68,9 @@ *** HOL *** +* Fact consolidation: even_less_0_iff is subsumed by +double_add_less_zero_iff_single_add_less_zero (simp by default anyway). + * Discontinued old-fashioned "codegen" tool. Code generation can always be externally triggered using an appropriate ROOT file plus a corresponding theory. Parametrization is possible using environment variables, or