| changeset 70226 | accbd801fefa |
| parent 69605 | a96320074298 |
| child 70270 | 4065e3b0e5bf |
--- 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>