src/HOL/Library/Word.thy
changeset 28229 4f06fae6a55e
parent 27487 c8a6ce181805
child 28562 4e74209f113e
--- a/src/HOL/Library/Word.thy	Tue Sep 16 09:21:24 2008 +0200
+++ b/src/HOL/Library/Word.thy	Tue Sep 16 09:21:26 2008 +0200
@@ -2267,6 +2267,8 @@
   fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
     fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
 
+declare fast_bv_to_nat_helper.simps [code func del]
+
 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
     fast_bv_to_nat_helper bs (Int.Bit0 bin)"
   by simp