changeset 13042 | d8a345d9e067 |
parent 13025 | 433c57d09d53 |
child 13158 | 8e86582a90d1 |
--- a/NEWS Thu Mar 07 22:52:07 2002 +0100 +++ b/NEWS Thu Mar 07 23:21:19 2002 +0100 @@ -210,7 +210,7 @@ - remove all special provisions on numerals in proofs; -* HOL: simp rules nat_number_of expand numerals on nat to Suc/0 +* HOL: simp rules nat_number expand numerals on nat to Suc/0 representation (depends on bin_arith_simps in the default context); * HOL: symbolic syntax for x^2 (numeral 2);