changeset 31720 | d1ac3f3b2f54 |
parent 31643 | b040f1679f77 |
child 31726 | ffd2dc631d88 |
--- a/NEWS Fri Jun 19 18:33:10 2009 +0200 +++ b/NEWS Fri Jun 19 18:56:53 2009 +0200 @@ -43,6 +43,8 @@ * Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions Set.Pow_def and Set.image_def. INCOMPATIBILITY. +* NewNumberTheory: Jeremy Avigad's new version of part of NumberTheory. +If possible, use NewNumberTheory, not NumberTheory. *** ML ***