src/HOL/Int.thy
changeset 66035 de6cd60b1226
parent 64996 b316cd527a11
child 66816 212a3334e7da
     1.1 --- a/src/HOL/Int.thy	Wed Jun 07 23:23:48 2017 +0200
     1.2 +++ b/src/HOL/Int.thy	Thu Jun 08 23:37:01 2017 +0200
     1.3 @@ -1713,11 +1713,7 @@
     1.4    "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
     1.5    "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
     1.6    "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
     1.7 -          apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
     1.8 -        apply (simp_all only: algebra_simps minus_diff_eq)
     1.9 -  apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
    1.10 -  apply (simp_all only: minus_add add.assoc left_minus)
    1.11 -  done
    1.12 +  by (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
    1.13  
    1.14  text \<open>Implementations.\<close>
    1.15