changeset 47818 | 151d137f1095 |
parent 47613 | e72e44cee6f2 |
child 48759 | ff570720ba1c |
--- a/src/HOL/IMP/Abs_Int0.thy Fri Apr 27 23:17:58 2012 +0200 +++ b/src/HOL/IMP/Abs_Int0.thy Sat Apr 28 07:38:22 2012 +0200 @@ -332,7 +332,7 @@ by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update split: option.splits del:subsetD) next - case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi) + case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq) by (metis le_post post_map_acom) next case (If b C1 C2 P)