--- a/NEWS Wed Dec 19 22:33:44 2007 +0100
+++ b/NEWS Wed Dec 19 22:34:03 2007 +0100
@@ -16,10 +16,11 @@
*** Pure ***
-* Command "instance" now takes list of definitions in the same manner
-as the "definition" command. Most notably, object equality is now
-possible. Type inference is more canonical than it used to be.
-INCOMPATIBILITY: in some cases explicit type annotations are required.
+* Instantiation target allows for simultaneous specification of class instance
+operations together with an instantiation proof. Type check phase allows to
+refer to class operations uniformly. See HOL/Complex/Complex.thy for an Isar
+example and HOL/Library/Eval.thy for an ML example.
+Superseedes some immature attempts.
*** HOL ***