--- a/NEWS Mon Sep 13 09:29:43 2010 +0200
+++ b/NEWS Mon Sep 13 14:53:56 2010 +0200
@@ -68,6 +68,9 @@
* Discontinued ancient 'constdefs' command. INCOMPATIBILITY, use
'definition' instead.
+* Document antiquotations 'class' and 'type' for printing classes
+and type constructors.
+
*** HOL ***