# HG changeset patch # User wenzelm # Date 954422039 -7200 # Node ID 8ba0f90f6f35bb5f6e078266c3b2ab6fda8de514 # Parent 3786d47f5570127b6df55595e457b3a9b7071a9d * Isar/Pure: local results and corresponding term bindings are now subject to Hindley-Milner polymorphism (similar to ML); this accommodates incremental type-inference nicely; * Isar/Pure: new calculational elements 'moreover' and 'ultimately' support plain accumulation of results, without applying any rules yet; diff -r 3786d47f5570 -r 8ba0f90f6f35 NEWS --- a/NEWS Thu Mar 30 15:13:02 2000 +0200 +++ b/NEWS Thu Mar 30 15:13:59 2000 +0200 @@ -33,18 +33,25 @@ *** Isar *** -* Pure now provides its own version of intro/elim/dest attributes; -useful for building new logics, but beware of confusion with the -Provers/classical ones; +* Pure: local results and corresponding term bindings are now subject +to Hindley-Milner polymorphism (similar to ML); this accommodates +incremental type-inference nicely; -* Pure: new 'obtain' language element supports generalized elimination -proofs; +* Pure: new 'obtain' language element supports generalized existence +reasoning; + +* Pure: new calculational elements 'moreover' and 'ultimately' support +plain accumulation of results, without applying any rules yet; * Pure: scalable support for case-analysis type proofs: new 'case' language element refers to local contexts symbolically, as produced by certain proof methods; internally, case names are attached to theorems as "tags"; +* Pure now provides its own version of intro/elim/dest attributes; +useful for building new logics, but beware of confusion with the +Provers/classical ones; + * Provers: splitter support (via 'split' attribute and 'simp' method modifier); 'simp' method: 'only:' modifier removes loopers as well (including splits);