NEWS
changeset 13042 d8a345d9e067
parent 13025 433c57d09d53
child 13158 8e86582a90d1
     1.1 --- a/NEWS	Thu Mar 07 22:52:07 2002 +0100
     1.2 +++ b/NEWS	Thu Mar 07 23:21:19 2002 +0100
     1.3 @@ -210,7 +210,7 @@
     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 +* HOL: simp rules nat_number expand numerals on nat to Suc/0
     1.9  representation (depends on bin_arith_simps in the default context);
    1.10  
    1.11  * HOL: symbolic syntax for x^2 (numeral 2);