# HG changeset patch
# User haftmann
# Date 1163805612 -3600
# Node ID 4058f08864487f877157acc28ce9e4f0f4465553
# Parent  26b51f724fe6ed3dbb8fed20492bae11a538469f
adjustments for class package

diff -r 26b51f724fe6 -r 4058f0886448 NEWS
--- a/NEWS	Fri Nov 17 17:32:30 2006 +0100
+++ b/NEWS	Sat Nov 18 00:20:12 2006 +0100
@@ -487,6 +487,13 @@
 
 *** HOL ***
 
+* New syntactic class "size"; overloaded constant "size" now
+has type "'a::size ==> bool"
+
+* Constants "Divides.op div", "Divides.op mod" and "Divides.op dvd" no named
+  "Divides.div", "Divides.mod" and "Divides.dvd"
+  INCOMPATIBILITY for ML code directly refering to constant names.
+
 * Replaced "auto_term" by the conceptually simpler method "relation",
 which just applies the instantiated termination rule with no further
 simplifications.