--- a/NEWS Tue Feb 11 12:55:35 2020 +0000
+++ b/NEWS Tue Feb 11 15:39:05 2020 +0100
@@ -109,6 +109,13 @@
* Antiquotation @{oracle_name} inlines a formally checked oracle name.
+* Minimal support for a soft-type system within the Isabelle logical
+framework (module Soft_Type_System).
+
+* Former Proof_Context.auto_fixes has been replaced by slightly more
+general Proof_Context.augment: it is subject to an optional soft-type
+system of the underlying object-logic. Minor INCOMPATIBILITY.
+
*** System ***