--- a/NEWS Tue Apr 27 21:34:22 2010 +0200
+++ b/NEWS Tue Apr 27 21:46:10 2010 +0200
@@ -295,6 +295,14 @@
*** ML ***
+* Sorts.certify_sort and derived "cert" operations for types and terms
+no longer minimize sorts. Thus certification at the boundary of the
+inference kernel becomes invariant under addition of class relations,
+which is an important monotonicity principle. Sorts are now minimized
+in the syntax layer only, at the boundary between the end-user and the
+system. Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort
+explicitly in rare situations.
+
* Antiquotations for basic formal entities:
@{class NAME} -- type class