# HG changeset patch
# User nipkow
# Date 1245435766 -7200
# Node ID caa89b41dcf267da5827495116c185e5d6222094
# Parent  d1ac3f3b2f54385a3af4475fa728199bfeb6409d# Parent  b03270a8c23f5b2d20a46c933dc7b9425c32bb32
merged

diff -r b03270a8c23f -r caa89b41dcf2 NEWS
--- a/NEWS	Fri Jun 19 20:22:28 2009 +0200
+++ b/NEWS	Fri Jun 19 20:22:46 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 ***