NEWS
changeset 6141 a6922171b396
parent 6131 2d9e609abcdb
child 6155 e387d188d0ca
     1.1 --- a/NEWS	Tue Jan 19 11:16:39 1999 +0100
     1.2 +++ b/NEWS	Tue Jan 19 11:18:11 1999 +0100
     1.3 @@ -11,6 +11,10 @@
     1.4  * ZF: The con_defs part of an inductive definition may no longer refer to 
     1.5    constants declared in the same theory;
     1.6  
     1.7 +* HOL, ZF: the function mk_cases, generated by the inductive definition 
     1.8 +  package, has lost an argument.  To simplify its result, it uses the default
     1.9 +  simpset instead of a supplied list of theorems.
    1.10 +
    1.11  
    1.12  *** Proof tools ***
    1.13  
    1.14 @@ -68,6 +72,9 @@
    1.15  
    1.16  * the datatype declaration of type T now defines the recursor T_rec;
    1.17  
    1.18 +* simplification automatically does freeness reasoning for datatype
    1.19 +  constructors;
    1.20 +
    1.21  * The syntax "if P then x else y" is now available in addition to if(P,x,y).
    1.22  
    1.23