src/HOL/Num.thy
changeset 66936 cf8d8fc23891
parent 66283 adf3155c57e2
child 67116 7397a6df81d8
     1.1 --- a/src/HOL/Num.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Num.thy	Mon Oct 30 13:18:41 2017 +0000
     1.3 @@ -522,6 +522,10 @@
     1.4  lemma mult_2_right: "z * 2 = z + z"
     1.5    by (simp add: one_add_one [symmetric] distrib_left)
     1.6  
     1.7 +lemma left_add_twice:
     1.8 +  "a + (a + b) = 2 * a + b"
     1.9 +  by (simp add: mult_2 ac_simps)
    1.10 +
    1.11  end
    1.12  
    1.13