--- a/NEWS Tue Apr 12 13:49:37 2016 +0200
+++ b/NEWS Tue Apr 12 14:38:57 2016 +0200
@@ -9,6 +9,13 @@
*** General ***
+* Type-inference improves sorts of newly introduced type variables for
+the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
+Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
+produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
+INCOMPATIBILITY, need to provide explicit type constraints for Pure
+types where this is really intended.
+
* Mixfix annotations support general block properties, with syntax
"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
"unbreakable", "markup". The existing notation "(DIGITS" is equivalent