# HG changeset patch
# User wenzelm
# Date 1581431945 -3600
# Node ID 2e1b0ee920f5cc6544245bc2c1fb3f50adc1a2f6
# Parent  d8fb621fea025baffe9a1a67f99e46287c4dae0e
updated for release;

diff -r d8fb621fea02 -r 2e1b0ee920f5 CONTRIBUTORS
--- 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
diff -r d8fb621fea02 -r 2e1b0ee920f5 NEWS
--- 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 ***