updated for release;
authorwenzelm
Tue Feb 11 15:39:05 2020 +0100 (2 weeks ago)
changeset 714362e1b0ee920f5
parent 71435 d8fb621fea02
child 71437 8fd1936490bc
updated for release;
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Feb 11 12:55:35 2020 +0000
     1.2 +++ b/CONTRIBUTORS	Tue Feb 11 15:39:05 2020 +0100
     1.3 @@ -23,6 +23,10 @@
     1.4  * February 2020: E. Gunther, M. Pagano and P. Sánchez Terraf
     1.5    Simplified, generalised version of ZF/Constructible.
     1.6  
     1.7 +* July 2019: Alexander Krauss, Makarius Wenzel
     1.8 +  Minimal support for a soft-type system within the Isabelle logical
     1.9 +  framework.
    1.10 +
    1.11  
    1.12  
    1.13  Contributions to Isabelle2019
     2.1 --- a/NEWS	Tue Feb 11 12:55:35 2020 +0000
     2.2 +++ b/NEWS	Tue Feb 11 15:39:05 2020 +0100
     2.3 @@ -109,6 +109,13 @@
     2.4  
     2.5  * Antiquotation @{oracle_name} inlines a formally checked oracle name.
     2.6  
     2.7 +* Minimal support for a soft-type system within the Isabelle logical
     2.8 +framework (module Soft_Type_System).
     2.9 +
    2.10 +* Former Proof_Context.auto_fixes has been replaced by slightly more
    2.11 +general Proof_Context.augment: it is subject to an optional soft-type
    2.12 +system of the underlying object-logic. Minor INCOMPATIBILITY.
    2.13 +
    2.14  
    2.15  *** System ***
    2.16