src/HOL/Int.thy
changeset 63648 f9f3006a5579
parent 63539 70d4d9e5707b
child 63652 804b80a80016
     1.1 --- a/src/HOL/Int.thy	Tue Aug 09 23:29:54 2016 +0200
     1.2 +++ b/src/HOL/Int.thy	Wed Aug 10 09:33:54 2016 +0200
     1.3 @@ -1190,7 +1190,7 @@
     1.4  apply (case_tac "k = f (Suc n)")
     1.5  apply force
     1.6  apply (erule impE)
     1.7 - apply (simp add: abs_if split add: if_split_asm)
     1.8 + apply (simp add: abs_if split: if_split_asm)
     1.9  apply (blast intro: le_SucI)
    1.10  done
    1.11