src/HOL/Library/Log_Nat.thy

--- a/src/HOL/Library/Log_Nat.thy	Sat Feb 03 20:46:28 2018 +0100
+++ b/src/HOL/Library/Log_Nat.thy	Mon Feb 05 08:30:19 2018 +0100
@@ -200,8 +200,11 @@
 lemma bitlen_alt_def: "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
 by (simp add: bitlen_def floorlog_def)
 
+lemma bitlen_zero[simp]: "bitlen 0 = 0"
+  by (auto simp: bitlen_def floorlog_def)
+
 lemma bitlen_nonneg: "0 \<le> bitlen x"
-by (simp add: bitlen_def)
+  by (simp add: bitlen_def)
 
 lemma bitlen_bounds:
   assumes "x > 0"