src/HOL/IMP/Def_Ass_Sound_Big.thy
changeset 45015 fdac1e9880eb
parent 43158 686fa0a0696e
child 47818 151d137f1095
     1.1 --- a/src/HOL/IMP/Def_Ass_Sound_Big.thy	Tue Sep 20 05:47:11 2011 +0200
     1.2 +++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy	Tue Sep 20 05:48:23 2011 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  theorem Sound:
     1.5    "\<lbrakk> (c,Some s) \<Rightarrow> s';  D A c A';  A \<subseteq> dom s \<rbrakk>
     1.6    \<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"
     1.7 -proof (induct c "Some s" s' arbitrary: s A A' rule:big_step_induct)
     1.8 +proof (induction c "Some s" s' arbitrary: s A A' rule:big_step_induct)
     1.9    case AssignNone thus ?case
    1.10      by auto (metis aval_Some option.simps(3) subset_trans)
    1.11  next