NEWS
changeset 12837 74ce01905e57
parent 12832 c31b44286a8a
child 12850 d3c16021e999
     1.1 --- a/NEWS	Wed Jan 23 11:43:53 2002 +0100
     1.2 +++ b/NEWS	Wed Jan 23 16:57:33 2002 +0100
     1.3 @@ -184,6 +184,9 @@
     1.4  
     1.5    - remove all special provisions on numerals in proofs;
     1.6  
     1.7 +* HOL: simp rules nat_number_of expand numerals on nat to Suc/0
     1.8 +representation (depends on bin_arith_simps in the default context);
     1.9 +
    1.10  * HOL: symbolic syntax for x^2 (numeral 2);
    1.11  
    1.12  * HOL: the class of all HOL types is now called "type" rather than