Declared nat_number_of as code lemma.

--- a/src/HOL/Integ/NatBin.thy	Wed Sep 21 12:01:31 2005 +0200
+++ b/src/HOL/Integ/NatBin.thy	Wed Sep 21 12:02:19 2005 +0200
@@ -28,6 +28,8 @@
 lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
 by (simp add: nat_number_of_def)
 
+declare nat_number_of [symmetric, THEN eq_reflection, code unfold]
+
 lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
 by (simp add: nat_number_of_def)