--- a/CONTRIBUTORS Tue Feb 11 12:55:35 2020 +0000
+++ b/CONTRIBUTORS Tue Feb 11 15:39:05 2020 +0100
@@ -23,6 +23,10 @@
* February 2020: E. Gunther, M. Pagano and P. Sánchez Terraf
Simplified, generalised version of ZF/Constructible.
+* July 2019: Alexander Krauss, Makarius Wenzel
+ Minimal support for a soft-type system within the Isabelle logical
+ framework.
+
Contributions to Isabelle2019
--- 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 ***