changeset 47818 | 151d137f1095 |
parent 45015 | fdac1e9880eb |
--- 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