| changeset 27106 | ff27dc6e7d05 |
| parent 26496 | 49ae9456eba9 |
| child 27368 | 9f90ac19e32b |
--- a/src/HOL/Library/Word.thy Tue Jun 10 15:30:54 2008 +0200 +++ b/src/HOL/Library/Word.thy Tue Jun 10 15:30:56 2008 +0200 @@ -2042,7 +2042,7 @@ definition length_nat :: "nat => nat" where - "length_nat x = (LEAST n. x < 2 ^ n)" + [code func del]: "length_nat x = (LEAST n. x < 2 ^ n)" lemma length_nat: "length (nat_to_bv n) = length_nat n" apply (simp add: length_nat_def)