diff -r 5d2d63f4363e -r 151d137f1095 src/HOL/IMP/Def_Ass_Sound_Big.thy --- a/src/HOL/IMP/Def_Ass_Sound_Big.thy Fri Apr 27 23:17:58 2012 +0200 +++ b/src/HOL/IMP/Def_Ass_Sound_Big.thy Sat Apr 28 07:38:22 2012 +0200 @@ -16,7 +16,7 @@ case AssignNone thus ?case by auto (metis aval_Some option.simps(3) subset_trans) next - case Semi thus ?case by auto metis + case Seq thus ?case by auto metis next case IfTrue thus ?case by auto blast next