| changeset 12837 | 74ce01905e57 |
| parent 12832 | c31b44286a8a |
| child 12850 | d3c16021e999 |
--- a/NEWS Wed Jan 23 11:43:53 2002 +0100 +++ b/NEWS Wed Jan 23 16:57:33 2002 +0100 @@ -184,6 +184,9 @@ - remove all special provisions on numerals in proofs; +* HOL: simp rules nat_number_of 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); * HOL: the class of all HOL types is now called "type" rather than