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