src/HOL/MicroJava/DFA/LBVCorrect.thy

   assumes pc:  "pc+1 < length ins"
   shows "wtl (take (pc+1) ins) c 0 s0 \<sqsubseteq>\<^sub>r \<phi>!(pc+1)"
 proof -
   from all pc
   have "wtc c (pc+1) (wtl (take (pc+1) ins) c 0 s0) \<noteq> T" by (rule wtl_all)
-  with pc show ?thesis by (simp add: phi_def wtc split: split_if_asm)
+  with pc show ?thesis by (simp add: phi_def wtc split: if_split_asm)
 qed
 
 
 lemma (in lbvs) wtl_stable:
   assumes wtl: "wtl ins c 0 s0 \<noteq> \<top>" 

     by (simp add: phi_def)
   from pc have c_None: "c!pc = \<bottom> \<Longrightarrow> \<phi>!pc = ?s1" ..
 
   from wt_s1 pc c_None c_Some
   have inst: "wtc c pc ?s1  = wti c pc (\<phi>!pc)"
-    by (simp add: wtc split: split_if_asm)
+    by (simp add: wtc split: if_split_asm)
 
   from pres cert s0 wtl pc have "?s1 \<in> A" by (rule wtl_pres)
   with pc c_Some cert c_None
   have "\<phi>!pc \<in> A" by (cases "c!pc = \<bottom>") (auto dest: cert_okD1)
   with pc pres

   case False
   with 0 have "phi!0 = c!0" ..
   moreover 
   from wtl have "wtl (take 1 ins) c 0 s0 \<noteq> \<top>"  by (rule wtl_take)
   with 0 False 
-  have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: split_if_asm)
+  have "s0 <=_r c!0" by (auto simp add: neq_Nil_conv wtc split: if_split_asm)
   ultimately
   show ?thesis by simp
 qed