changeset 47818 | 151d137f1095 |
parent 45200 | 1f1897ac7877 |
child 52046 | bc01725d7918 |
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Fri Apr 27 23:17:58 2012 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Sat Apr 28 07:38:22 2012 +0200 @@ -187,7 +187,7 @@ case Assign thus ?case by (auto simp: lookup_update aval'_sound) next - case Semi thus ?case by fastforce + case Seq thus ?case by fastforce next case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound) next