NEWS
changeset 8621 8ba0f90f6f35
parent 8603 805910de7be0
child 8626 76e3913ff421
     1.1 --- a/NEWS	Thu Mar 30 15:13:02 2000 +0200
     1.2 +++ b/NEWS	Thu Mar 30 15:13:59 2000 +0200
     1.3 @@ -33,18 +33,25 @@
     1.4  
     1.5  *** Isar ***
     1.6  
     1.7 -* Pure now provides its own version of intro/elim/dest attributes;
     1.8 -useful for building new logics, but beware of confusion with the
     1.9 -Provers/classical ones;
    1.10 +* Pure: local results and corresponding term bindings are now subject
    1.11 +to Hindley-Milner polymorphism (similar to ML); this accommodates
    1.12 +incremental type-inference nicely;
    1.13  
    1.14 -* Pure: new 'obtain' language element supports generalized elimination
    1.15 -proofs;
    1.16 +* Pure: new 'obtain' language element supports generalized existence
    1.17 +reasoning;
    1.18 +
    1.19 +* Pure: new calculational elements 'moreover' and 'ultimately' support
    1.20 +plain accumulation of results, without applying any rules yet;
    1.21  
    1.22  * Pure: scalable support for case-analysis type proofs: new 'case'
    1.23  language element refers to local contexts symbolically, as produced by
    1.24  certain proof methods; internally, case names are attached to theorems
    1.25  as "tags";
    1.26  
    1.27 +* Pure now provides its own version of intro/elim/dest attributes;
    1.28 +useful for building new logics, but beware of confusion with the
    1.29 +Provers/classical ones;
    1.30 +
    1.31  * Provers: splitter support (via 'split' attribute and 'simp' method
    1.32  modifier); 'simp' method: 'only:' modifier removes loopers as well
    1.33  (including splits);