src/ZF/Int_ZF.thy
changeset 59788 6f7b6adac439
parent 58871 c399ae4b836f
child 60770 240563fbf41d
     1.1 --- a/src/ZF/Int_ZF.thy	Mon Mar 23 19:43:03 2015 +0100
     1.2 +++ b/src/ZF/Int_ZF.thy	Mon Mar 23 21:05:17 2015 +0100
     1.3 @@ -661,7 +661,7 @@
     1.4  apply (simp add: zless_def znegative_def zdiff_def int_def)
     1.5  apply (auto dest!: less_imp_succ_add simp add: zadd zminus int_of_def)
     1.6  apply (rule_tac x = k in bexI)
     1.7 -apply (erule_tac i="succ (?v)" in add_left_cancel, auto)
     1.8 +apply (erule_tac i="succ (v)" for v in add_left_cancel, auto)
     1.9  done
    1.10  
    1.11  lemma zless_imp_succ_zadd: