diff -r 129757af1096 -r accbd801fefa src/HOL/Num.thy
--- a/src/HOL/Num.thy	Wed May 01 10:40:40 2019 +0000
+++ b/src/HOL/Num.thy	Wed May 01 10:40:42 2019 +0000
@@ -229,6 +229,10 @@
 lemma sqr_conv_mult: "sqr x = x * x"
   by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult)
 
+lemma num_double [simp]:
+  "num.Bit0 num.One * n = num.Bit0 n"
+  by (simp add: num_eq_iff nat_of_num_mult)
+
 
 subsection \<open>Binary numerals\<close>