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