src/HOL/IMP/Def_Ass_Sound_Small.thy

     by(cases bv)(auto intro: small_step.IfTrue small_step.IfFalse)
 qed (fastforce intro: small_step.intros)+
 
 lemma D_mono:  "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
 proof (induction c arbitrary: A A' M)
-  case Semi thus ?case by auto (metis D.intros(3))
+  case Seq thus ?case by auto (metis D.intros(3))
 next
   case (If b c1 c2)
   then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
     by auto
   with If.IH `A \<subseteq> A'` obtain M1' M2'

   case (While b c s)
   then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
   moreover
   then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
   ultimately have "D (dom s) (IF b THEN c; WHILE b DO c ELSE SKIP) (dom s)"
-    by (metis D.If[OF `vars b \<subseteq> dom s` D.Semi[OF `D (dom s) c A'` D.While[OF _ `D A' c A''`]] D.Skip] D_incr Int_absorb1 subset_trans)
+    by (metis D.If[OF `vars b \<subseteq> dom s` D.Seq[OF `D (dom s) c A'` D.While[OF _ `D A' c A''`]] D.Skip] D_incr Int_absorb1 subset_trans)
   thus ?case by (metis D_incr `A = dom s`)
 next
-  case Semi2 thus ?case by auto (metis D_mono D.intros(3))
+  case Seq2 thus ?case by auto (metis D_mono D.intros(3))
 qed (auto intro: D.intros)
 
 theorem D_sound:
   "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A' \<Longrightarrow> c' \<noteq> SKIP
    \<Longrightarrow> \<exists>cs''. (c',s') \<rightarrow> cs''"