# HG changeset patch
# User berghofe
# Date 1127816166 -7200
# Node ID 8ef257366a0ce6b39cf6129868d31478be65d0ae
# Parent  2beb71c0f92e4b1e4166dc3444e1aab894d01095
nat_number_of is no longer declared as code lemma, since this turned
out to be too inefficient.

diff -r 2beb71c0f92e -r 8ef257366a0c src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Tue Sep 27 12:14:39 2005 +0200
+++ b/src/HOL/Integ/NatBin.thy	Tue Sep 27 12:16:06 2005 +0200
@@ -28,8 +28,6 @@
 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)