# HG changeset patch
# User berghofe
# Date 1127296939 -7200
# Node ID 9bcd6ea262b839e66ec9a37cac3cc8cdee725859
# Parent  ee4408eac12c9ee16e5f7417b44032d1048e6c5c
Declared nat_number_of as code lemma.

diff -r ee4408eac12c -r 9bcd6ea262b8 src/HOL/Integ/NatBin.thy
--- 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)