# HG changeset patch
# User nipkow
# Date 1245430613 -7200
# Node ID d1ac3f3b2f54385a3af4475fa728199bfeb6409d
# Parent  29f5b20e8ee86504b3b91fc96761ad82b99b2ff8
NewNumberTheory

diff -r 29f5b20e8ee8 -r d1ac3f3b2f54 NEWS
--- 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 ***