src/HOL/IMP/Abs_Int0.thy
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)