changeset 47818 | 151d137f1095 |
parent 45212 | e87feee00a4c |
child 48480 | cb03acfae211 |
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Fri Apr 27 23:17:58 2012 +0200 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Sat Apr 28 07:38:22 2012 +0200 @@ -160,7 +160,7 @@ next case Assign thus ?case by (auto simp: aval'_sound) next - case Semi thus ?case by auto + case Seq thus ?case by auto next case If thus ?case by(auto simp: in_rep_join) next