misc;
authorwenzelm
Thu Nov 30 20:03:39 2000 +0100 (2000-11-30)
changeset 10547efaba354b7f1
parent 10546 b0ad1ed24cf6
child 10548 e8c774c12105
misc;
NEWS
     1.1 --- a/NEWS	Thu Nov 30 17:55:17 2000 +0100
     1.2 +++ b/NEWS	Thu Nov 30 20:03:39 2000 +0100
     1.3 @@ -32,6 +32,12 @@
     1.4  
     1.5  *** Isar ***
     1.6  
     1.7 +* Pure: Isar now suffers initial goal statements to contain unbound
     1.8 +schematic variables (this does not conform to actual readable proof
     1.9 +documents, due to unpredictable outcome and non-compositional proof
    1.10 +checking); users who know what they are doing may use schematic goals
    1.11 +for Prolog-style synthesis of proven results;
    1.12 +
    1.13  * Pure: assumption method (an implicit finishing) now handles actual
    1.14  rules as well;
    1.15  
    1.16 @@ -49,6 +55,10 @@
    1.17  * HOL: improved method 'induct' --- now handles non-atomic goals
    1.18  (potential INCOMPATIBILITY); tuned error handling;
    1.19  
    1.20 +* HOL: cases and induct rules may now provide explicit hint about the
    1.21 +number of facts to be consumed (0 for "type" and 1 for "set" rules);
    1.22 +any remaining facts are inserted into the goal verbatim;
    1.23 +
    1.24  
    1.25  *** HOL ***
    1.26  
    1.27 @@ -67,14 +77,20 @@
    1.28  
    1.29  *** CTT ***
    1.30  
    1.31 -* CTT: x-symbol support for Pi, Sigma, -->, : (membership)
    1.32 -  note that "lam" is displayed as TWO lambda-symbols
    1.33 +* CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that
    1.34 +"lam" is displayed as TWO lambda-symbols
    1.35  
    1.36 -* CTT: theory Main now available, containing everything
    1.37 -(that is, Bool and Arith) 
    1.38 +* CTT: theory Main now available, containing everything (that is, Bool
    1.39 +and Arith);
    1.40 +
    1.41  
    1.42  *** General ***
    1.43  
    1.44 +* Pure: the Simplifier has been implemented properly as a derived rule
    1.45 +outside of the actual kernel (at last!); the overall performance
    1.46 +penalty in practical applications is about 50%, while reliability of
    1.47 +the Isabelle inference kernel has been greatly improved;
    1.48 +
    1.49  * Provers: fast_tac (and friends) now handle actual object-logic rules
    1.50  as assumptions as well;
    1.51