# HG changeset patch
# User wenzelm
# Date 1011801453 -3600
# Node ID 74ce01905e5754c0c85d5f17a78dee25cee319d6
# Parent  5ef96e63fba6c9830394166d0fa82c0fc08152f6
* HOL: nat_number_of;

diff -r 5ef96e63fba6 -r 74ce01905e57 NEWS
--- 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