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