diff -r 0e847655b2d8 -r fdac1e9880eb src/HOL/IMP/Def_Ass_Sound_Big.thy --- a/src/HOL/IMP/Def_Ass_Sound_Big.thy Tue Sep 20 05:47:11 2011 +0200 +++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy Tue Sep 20 05:48:23 2011 +0200 @@ -12,7 +12,7 @@ theorem Sound: "\ (c,Some s) \ s'; D A c A'; A \ dom s \ \ \ t. s' = Some t \ A' \ dom t" -proof (induct c "Some s" s' arbitrary: s A A' rule:big_step_induct) +proof (induction c "Some s" s' arbitrary: s A A' rule:big_step_induct) case AssignNone thus ?case by auto (metis aval_Some option.simps(3) subset_trans) next