NEWS

--- a/NEWS	Tue Aug 14 11:37:58 2012 +0200
+++ b/NEWS	Tue Aug 14 11:43:08 2012 +0200
@@ -29,6 +29,12 @@
 operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
 with some care where this is really required.
 
+* Command 'typ' supports an additional variant with explicit sort
+constraint, to infer and check the most general type conforming to a
+given given sort.  Example (in HOL):
+
+  typ "_ * _ * bool * unit" :: finite
+
 
 *** HOL ***